@book{coq,
  title={Interactive theorem proving and program development: Coq’Art: the calculus of inductive constructions},
  author={Bertot, Yves and Cast{\'e}ran, Pierre},
  year={2013},
  publisher={Springer Science \& Business Media}
}

@book{isabelle,
  title={Isabelle: A generic theorem prover},
  author={Paulson, Lawrence C},
  volume={828},
  year={1994},
  publisher={Springer Science \& Business Media}
}

@phdthesis{agda,
  author  = {Norell, Ulf},
  title	  = {Towards a practical programming language based on dependent type theory},
  school  = {Department of Computer Science and Engineering, Chalmers University of Technology},
  year	  = 2007,
  month	  = {September},
  address = {SE-412 96 G\"{o}teborg, Sweden}
}

@Inbook{vampire,
author="Kov{\'a}cs, Laura and Voronkov, Andrei",
editor="Sharygina, Natasha
and Veith, Helmut",
title="First-Order Theorem Proving and Vampire",
bookTitle="Computer Aided Verification: 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings",
year="2013",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="1--35",
}

@techreport{rosu-2003-cs322,
    author = "Ro\c{s}u, Grigore",
    month = "December",
    year = "2003",
    number = "http://hdl.handle.net/2142/11385",
    institution = "University of Illinois",
    title = "{CS322 - Programming Language Design: Lecture Notes}"
}

@article{rosu-2017-lmcs,
    author = "Ro\c{s}u, Grigore",
    doi = "http://arxiv.org/abs/1705.06312",
    title = "Matching logic",
    journal = "Logical Methods in Computer Science",
    volume = "to appear",
    year = "2017",
    url = "http://arxiv.org/abs/1705.06312",
    project_acronym = "Matching Logic"
}

@misc{hiraidefining,
  title={Defining the Ethereum Virtual Machine for Interactive Theorem Provers},
  author={Hirai, Yoichi},
  howpublished = {WSTC17, International Conference on Financial Cryptography and Data Security},
  year={2017}
}

@techreport{hildenbrandt-saxena-zhu-rodrigues-daian-guth-rosu-2017-tr,
  author   = {Everett Hildenbrandt and Manasvi Saxena and Xiaoran Zhu and Nishant Rodrigues and Philip Daian and Dwight Guth and Grigore Rosu},
  title    = {KEVM: A Complete Semantics of the Ethereum Virtual Machine},
  institution = {University of Illinois},
  month       = {Aug},
  year        = {2017},
  number      = {http://hdl.handle.net/2142/97207},
}

@inproceedings{mulligan2014lem,
  title={Lem: reusable engineering of real-world semantics},
  author={Mulligan, Dominic P and Owens, Scott and Gray, Kathryn E and Ridge, Tom and Sewell, Peter},
  booktitle={ACM SIGPLAN Notices},
  volume={49},
  number={9},
  pages={175--188},
  year={2014},
  organization={ACM}
}

@inproceedings{smith-1984-popl,
  title={Reflection and semantics in {LISP}},
  author={Smith, Brian Cantwell},
  booktitle={POPL'84},
  pages={23-35},
  year={1984},
  organization={ACM}
}

@article{Plotkin:1970,
    author = {Plotkin, Gordon D.},
    journal = {Machine Intelligence},
    pages = {153-163},
    title = {{A note on inductive generalization}},
    volume = {5},
    year = {1970}
}

@book{Blackburn:2001:ML:381193,
 author = {Blackburn, Patrick and de Rijke, Maarten and Venema, Yde},
 title = {Modal Logic},
 year = {2001},
 isbn = {0-521-80200-8},
 publisher = {Cambridge University Press},
 address = {NY, USA},
}

@article{DBLP:journals/scp/CholewaEM15,
  author    = {Andrew Cholewa and
               Santiago Escobar and
               Jos{\'{e}} Meseguer},
  title     = {Constrained narrowing for conditional equational theories modulo axioms},
  journal   = {Science of Computer Programming},
  volume    = {112},
  pages     = {24-57},
  year      = {2015},
  url       = {http://dx.doi.org/10.1016/j.scico.2015.06.001},
  doi       = {10.1016/j.scico.2015.06.001},
  timestamp = {Wed, 13 Jan 2016 12:55:51 +0100},
  biburl    = {http://dblp2.uni-trier.de/rec/bib/journals/scp/CholewaEM15},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{DBLP:conf/lopstr/MeseguerS15,
  author    = {Jos{\'{e}} Meseguer and
               Stephen Skeirik},
  title     = {Equational Formulas and Pattern Operations in Initial Order-Sorted
               Algebras},
  booktitle = {LOPSTR'15},
  pages     = {36-53},
  year      = {2015},
  series    = {LNCS},
  volume    = {9527},
  publisher = {Springer},
  url       = {http://dx.doi.org/10.1007/978-3-319-27436-2_3},
  doi       = {10.1007/978-3-319-27436-2_3},
  timestamp = {Thu, 17 Dec 2015 16:14:52 +0100},
  biburl    = {http://dblp2.uni-trier.de/rec/bib/conf/lopstr/MeseguerS15},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@article{DBLP:journals/tcs/Pichler03,
  author    = {Reinhard Pichler},
  title     = {Explicit versus implicit representations of subsets of the {Herbrand}
               universe},
  journal   = {Theoretical Computer Science},
  volume    = {290},
  number    = {1},
  pages     = {1021-1056},
  year      = {2003},
  url       = {http://dx.doi.org/10.1016/S0304-3975(02)00583-2},
  doi       = {10.1016/S0304-3975(02)00583-2},
  timestamp = {Wed, 07 Sep 2011 12:13:21 +0200},
  biburl    = {http://dblp2.uni-trier.de/rec/bib/journals/tcs/Pichler03},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{DBLP:conf/rta/Tajine93,
  author    = {Mohamed Tajine},
  title     = {The Negation Elimination from Syntactic Equational Formula is Decidable},
  booktitle = {RTA'93},
  pages     = {316-327},
  year      = {1993},
  series    = {LNCS},
  volume    = {690},
  url       = {http://dx.doi.org/10.1007/3-540-56868-9_24},
  doi       = {10.1007/3-540-56868-9_24},
  timestamp = {Thu, 23 Jun 2016 15:53:28 +0200},
  biburl    = {http://dblp2.uni-trier.de/rec/bib/conf/rta/Tajine93},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{DBLP:conf/mfcs/LassezMM91,
  author    = {Jean{-}Louis Lassez and
               Michael J. Maher and
               Kim Marriott},
  title     = {Elimination of Negation in Term Algebras},
  booktitle = {{MFCS'91}},
  pages     = {1-16},
  year      = {1991},
  series    = {LNCS},
  volume    = {520},
  url       = {http://dx.doi.org/10.1007/3-540-54345-7_44},
  doi       = {10.1007/3-540-54345-7_44},
  timestamp = {Mon, 21 Sep 2009 14:00:20 +0200},
  biburl    = {http://dblp2.uni-trier.de/rec/bib/conf/mfcs/LassezMM91},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@article{DBLP:journals/jsc/Fernandez98,
  author    = {Maribel Fern{\'{a}}ndez},
  title     = {Negation Elimination in Empty or Permutative Theories},
  journal   = {Journal of Symbolic Computation},
  volume    = {26},
  number    = {1},
  pages     = {97-133},
  year      = {1998},
  url       = {http://dx.doi.org/10.1006/jsco.1998.0203},
  doi       = {10.1006/jsco.1998.0203},
  timestamp = {Tue, 20 Sep 2011 11:17:56 +0200},
  biburl    = {http://dblp2.uni-trier.de/rec/bib/journals/jsc/Fernandez98},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@article{DBLP:journals/jar/LassezM87,
  author    = {Jean{-}Louis Lassez and
               Kim Marriott},
  title     = {Explicit Representation of Terms Defined by Counter Examples},
  journal   = {Journal of Automated Reasoning},
  volume    = {3},
  number    = {3},
  pages     = {301-317},
  year      = {1987},
  url       = {http://dx.doi.org/10.1007/BF00243794},
  doi       = {10.1007/BF00243794},
  timestamp = {Thu, 19 May 2011 15:52:20 +0200},
  biburl    = {http://dblp2.uni-trier.de/rec/bib/journals/jar/LassezM87},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@book{Nipkow:2002:IPA:1791547,
 author = {Nipkow, Tobias and Wenzel, Markus and Paulson, Lawrence C.},
 title = {Isabelle/HOL: A Proof Assistant for Higher-order Logic},
 year = {2002},
 isbn = {3-540-43376-7},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
}

@Manual{Coq:manual,
  title =        {The Coq proof assistant reference manual},
  author =       {\mbox{The Coq development team}},
  organization = {LogiCal Project},
  note =         {Version 8.0, \url{http://coq.inria.fr}},
  year =         {2004},
}



@InProceedings{ott-icfp,
  title =	"Ott: effective tool support for the working
		 semanticist",
  author =	"Peter Sewell and Francesco Zappa Nardelli and Scott
		 Owens and Gilles Peskine and Tom Ridge and Susmit
		 Sarkar and Rok Strnisa",
  bibdate =	"2007-11-06",
  bibsource =	"DBLP,
		 http://dblp.uni-trier.de/db/conf/icfp/icfp2007.html#SewellNOPRSS07",
  booktitle =	"ICFP'07",
  year =        "2007",
  publisher =	"ACM",
  ISBN = 	"978-1-59593-815-2",
  pages =	"1-12",
  doi =         "10.1017/S0956796809990293",
}

@inproceedings{plt-redex,
 author = {Klein, Casey and Clements, John and Dimoulas, Christos and Eastlund, Carl and Felleisen, Matthias and Flatt, Matthew and McCarthy, Jay A. and Rafkind, Jon and Tobin-Hochstadt, Sam and Findler, Robert Bruce},
 title = {Run Your Research: On the Effectiveness of Lightweight Mechanization},
 booktitle = {POPL'12},
 year={2012},
 isbn = {978-1-4503-1083-3},
 location = {Philadelphia, PA, USA},
 pages = {285-296},
 numpages = {12},
 doi = {10.1145/2103656.2103691},
 acmid = {2103691},
 publisher = {ACM},
 keywords = {lightweight semantics engineering},
}

@inproceedings{caml-ott,
 author = {Owens, Scott},
 title = {A Sound Semantics for {OC}aml$_{\mathit{light}}$},
 booktitle = {ESOP'08},
 series={LNCS},
 volume = {4960},
 year = {2008},
 isbn = {978-3-540-78738-9},
 pages = {1-15},
 numpages = {15},
 doi = {10.1007/978-3-540-78739-6_1},
}

@inproceedings{k-php,
isbn={978-3-662-44201-2},
booktitle={ECOOP'14},
series={LNCS},
year={2014},
doi={10.1007/978-3-662-44202-9_23},
title={An Executable Formal Semantics of PHP},
publisher={Springer},
author={Filaretti, Daniele and Maffeis, Sergio},
pages={567-592},
language={English}
}

@inproceedings{pltredex-python,
 author = {Politz, Joe Gibbs and Martinez, Alejandro and Milano, Matthew and Warren, Sumner and Patterson, Daniel and Li, Junsong and Chitipothu, Anand and Krishnamurthi, Shriram},
 title = {Python: The Full Monty},
 booktitle = {OOPSLA'13},
 year = {2013},
 isbn = {978-1-4503-2374-1},
 pages = {217-232},
 numpages = {16},
 doi = {10.1145/2509136.2509536},
 acmid = {2509536},
 publisher = {ACM},
 keywords = {serpents},
}

@inproceedings{bodin-etal-javascript,
 author = {Bodin, Martin and Chargueraud, Arthur and Filaretti, Daniele and Gardner, Philippa and Maffeis, Sergio and Naudziuniene, Daiva and Schmitt, Alan and Smith, Gareth},
 title = {A Trusted Mechanised {J}ava{S}cript Specification},
 booktitle = {POPL'14},
 year = {2014},
 isbn = {978-1-4503-2544-8},
 location = {San Diego, California, USA},
 pages = {87-100},
 numpages = {14},
 doi = {10.1145/2535838.2535876},
 acmid = {2535876},
 publisher = {ACM},
 keywords = {coq, javascript, mechanised semantics},
}

@inproceedings{DBLP:conf/tacas/Beyer16,
  author    = {Dirk Beyer},
  title     = {Reliable and Reproducible Competition Results with BenchExec and Witnesses
               (Report on {SV-COMP} 2016)},
  booktitle = {TACAS'16},
  series    = {LNCS},
  volume    = {9636},
  pages     = {887-904},
  year      = {2016},
}

@Inproceedings{Calcagno2005,
author="Calcagno, Cristiano
and Gardner, Philippa
and Hague, Matthew",
title="From Separation Logic to First-Order Logic",
bookTitle="FOSSACS'05",
year="2005",
pages="395-409",
series="LNCS",
volume="3441",
isbn="978-3-540-31982-5",
doi="10.1007/978-3-540-31982-5_25",
url="http://dx.doi.org/10.1007/978-3-540-31982-5_25"
}

@inproceedings{Bobot2012,
author="Bobot, Fran{\c{c}}ois
and Filli{\^a}tre, Jean-Christophe",
title="Separation Predicates: A Taste of Separation Logic in First-Order Logic",
bookTitle="ICFEM'12",
year="2012",
pages="167-181",
series="LNCS",
volume="7635",
isbn="978-3-642-34281-3",
doi="10.1007/978-3-642-34281-3_14",
url="http://dx.doi.org/10.1007/978-3-642-34281-3_14"
}

@article{10.1109/SKG.2010.29,
author = {Cungen Cao and Ju Wang and Yuefei Sui and Yuming Shen},
title = {Translating Separation Logic into a Fragment of the First-Order Logic},
journal = {International Conference on Semantics, Knowledge and Grid},
year = {2010},
pages = {188-194},
doi = {doi.ieeecomputersociety.org/10.1109/SKG.2010.29},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}

@inproceedings{Piskac:2013:ASL:2526861.2526927,
 author = {Piskac, Ruzica and Wies, Thomas and Zufferey, Damien},
 title = {Automating Separation Logic Using SMT},
 booktitle = {CAV'13},
 series = {LNCS},
 volume = {8044},
 year = {2013},
 isbn = {978-3-642-39798-1},
 pages = {773-789},
 numpages = {17},
 url = {http://dx.doi.org/10.1007/978-3-642-39799-8_54},
 doi = {10.1007/978-3-642-39799-8_54},
 acmid = {2526927},
}

@inproceedings{Parkinson2011,
author="Parkinson, Matthew J.
and Summers, Alexander J.",
title="The Relationship between Separation Logic and Implicit Dynamic Frames",
bookTitle="ESOP'11",
year="2011",
series="LNCS",
volume="6602",
pages="439-458",
isbn="978-3-642-19718-5",
doi="10.1007/978-3-642-19718-5_23",
url="http://dx.doi.org/10.1007/978-3-642-19718-5_23"
}

@Inproceedings{Calcagno2001,
author="Calcagno, Cristiano
and Yang, Hongseok
and O'Hearn, Peter W.",
title="Computability and Complexity Results for a Spatial Assertion Language for Data Structures",
bookTitle="FSTTCS'01",
year="2001",
pages="108-119",
series="LNCS",
volume="2245",
isbn="978-3-540-45294-2",
doi="10.1007/3-540-45294-X_10",
url="http://dx.doi.org/10.1007/3-540-45294-X_10"
}

@book{vanBenthem1983-VANMLA,
	year = {1983},
	publisher = {Bibliopolis, Naples.  Distributed in the U.S.A. By Humanities Press},
	title = {Modal Logic and Classical Logic},
	author = {J. F. A. K. van Benthem}
}

@article{Goldblatt:2003:MML:969657.969658,
 author = {Goldblatt, Robert},
 title = {Mathematical Modal Logic: A View of Its Evolution},
 journal = {Journal of Applied Logic},
 volume = {1},
 number = {5-6},
 year = {2003},
 issn = {1570-8683},
 pages = {309-392},
 numpages = {84},
 url = {http://dx.doi.org/10.1016/S1570-8683(03)00008-9},
 doi = {10.1016/S1570-8683(03)00008-9},
 acmid = {969658},
 publisher = {Elsevier Science Publishers B. V.},
 address = {Amsterdam, The Netherlands, The Netherlands},
 keywords = {Boolean algebra, Kripke semantics, history of logic, modal logic},
}

@Book{nla.cat-vn2062435,
author = {Kreisel, Georg. and Krivine, J. L. },
title = {Elements of mathematical logic (Model theory)},
publisher = {North Holland Publishing Company, Amsterdam},
pages = { xi, 222 p. },
year = { 1967 },
}

@book{Harrison:2009:HPL:1540610,
 author = {Harrison, John},
 title = {Handbook of Practical Logic and Automated Reasoning},
 year = {2009},
 isbn = {0521899575, 9780521899574},
 edition = {1st},
 publisher = {Cambridge University Press},
 address = {New York, NY, USA},
}


@inproceedings{Brotherston:2014:DPS:2603088.2603091,
 author = {Brotherston, James and Fuhs, Carsten and P{\'e}rez, Juan A. Navarro and Gorogiannis, Nikos},
 title = {A Decision Procedure for Satisfiability in Separation Logic with Inductive Predicates},
 booktitle = {CSL-LICS'14},
 year = {2014},
 pages = {25:1-25:10},
 articleno = {25},
 numpages = {10},
 url = {http://doi.acm.org/10.1145/2603088.2603091},
 doi = {10.1145/2603088.2603091},
 acmid = {2603091},
 publisher = {ACM},
}

@inproceedings{Appel2007,
author = {Appel, AW and Blazy, Sandrine},
title = {{Separation logic for small-step Cminor}},
booktitle = {TPHOLs'07},
doi = {10.1007/978-3-540-74591-4_3},
isbn = {978-3-540-74590-7},
issn = {03029743},
pages = {5-21},
url = {http://arxiv.org/abs/0707.4389$\backslash$nhttp://link.springer.com/chapter/10.1007/978-3-540-74591-4{\_}3},
volume = {4732},
series={LNCS},
year = {2007}
}

@inproceedings{Berdine2005,
title = {{Smallfoot: Modular Automatic Assertion Checking with Separation Logic.}},
author = {Berdine, Josh and Calcagno, Cristiano and O'Hearn, Peter},
booktitle = {FMCO'05},
doi = {10.1007/11804192_6},
isbn = {978-3-540-36749-9},
issn = {03029743},
pages = {115-137},
series = {LNCS},
url = {http://discovery.ucl.ac.uk/1342330/},
volume = {4111},
year = {2005}
}

@inproceedings{Berdine2011,
title = {{SLAyer: Memory safety for systems-level code}},
author = {Berdine, Josh and Cook, Byron and Ishtiaq, Samin},
booktitle = {CAV'11},
doi = {10.1007/978-3-642-22110-1_15},
isbn = {9783642221095},
issn = {03029743},
pages = {178-183},
series = {LNCS},
volume = {6806},
year = {2011}
}

@article{Botincan2009,
author = {Botincan, Matko and Parkinson, Matthew and Schulte, Wolfram},
title = {{Separation Logic Verification of C Programs with an SMT Solver}},
pages = {5-23},
doi = {10.1016/j.entcs.2009.09.057},
issn = {15710661},
journal = {Electronic Notes in Theoretical Computer Science},
keywords = {C programming language,Separation logic,automated theorem proving,automated verification},
volume = {254},
year = {2009}
}

@inproceedings{NavarroPerez2013,
title = {{Separation logic modulo theories}},
author = {{Navarro Perez}, Juan Antonio and Rybalchenko, Andrey},
booktitle = {APLAS'13},
series = {LNCS},
volume = {8301},
pages = {90-106},
year = {2013}
}

@inproceedings{Perez2011,
title = {{Separation logic + superposition calculus = heap theorem prover}},
author = {{Navarro Perez}, Juan Antonio and Rybalchenko, Andrey},
booktitle = {PLDI'11},
pages = {556-566},
publisher = {ACM},
url = {http://dl.acm.org/citation.cfm?doid=1993316.1993563},
year = {2011}
}

@inproceedings{Brotherston2016,
author = {Brotherston, James and Gorogiannis, Nikos and Kanovich, Max and Rowe, Reuben},
booktitle = {POPL'16},
doi = {10.1145/2837614.2837621},
publisher = {ACM},
pages = {84-96},
title = {{Model Checking for Symbolic-Heap Separation Logic with Inductive Predicates}},
url = {http://dl.acm.org/citation.cfm?id=2837621},
year = {2016}
}

@inproceedings{Brotherston2014,
author = {Brotherston, James and Villard, Jules},
booktitle = {POPL'14},
publisher = {ACM},
doi = {10.1145/2535838.2535844},
pages = {453-464},
title = {{Parametric Completeness for Separation Theories}},
year = {2014}
}

@inproceedings{Chu2015,
author = {Chu, Duc-Hiep and Jaffar, Joxan and Trinh, Minh-Thai},
booktitle = {PLDI'15},
pages = {457-466},
publisher = {ACM},
title = {{Automatic Induction Proofs of Data-Structures in Imperative Programs}},
url = {http://dx.doi.org/10.1145/2737924.2737984},
year = {2015}
}

@inproceedings{Krebbers2017,
author = {Krebbers, Robbert and Timany, Amin and Birkedal, Lars},
booktitle = {POPL'17},
title = {{Interactive Proofs in Higher-Order Concurrent Separation Logic}},
pages = {457-466},
publisher = {ACM},
year = {2017}
}

@inproceedings{Pek2014,
author = {Pek, Edgar and Qiu, Xiaokang and Madhusudan, P},
booktitle = {PLDI'14},
pages = {440-451},
title = {{Natural Proofs for Data Structure Manipulation in C using Separation Logic}},
url = {http://dx.doi.org/10.1145/2594291.2594325},
publisher = {ACM},
year = {2014}
}

@inproceedings{Burstall:1977:PTT:1622943.1623045,
 author = {Burstall, R. M. and Goguen, J. A.},
 title = {Putting Theories Together to Make Specifications},
 booktitle = {IJCAI'77},
 year = {1977},
 pages = {1045-1058},
 numpages = {14},
 url = {http://dl.acm.org/citation.cfm?id=1622943.1623045},
 acmid = {1623045},
 publisher = {Morgan Kaufmann Publishers Inc.},
}

@article{Liskov:1974:PAD:942572.807045,
 author = {Liskov, Barbara and Zilles, Stephen},
 title = {Programming with Abstract Data Types},
 journal = {SIGPLAN Not.},
 issue_date = {April 1974},
 volume = {9},
 number = {4},
 month = mar,
 year = {1974},
 issn = {0362-1340},
 pages = {50-59},
 numpages = {10},
 url = {http://doi.acm.org/10.1145/942572.807045},
 doi = {10.1145/942572.807045},
 acmid = {807045},
 publisher = {ACM},
 address = {New York, NY, USA},
}

@misc{wikiADT,
   author = "Wikipedia",
   title = "Abstract Data Type",
   year = "2016",
   note = "\url{https://en.wikipedia.org/wiki/Abstract_data_type}",
}

@article{GOGUEN1992217,
author = "Joseph A. Goguen and Jose Meseguer",
title = "Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations",
journal = "Theoretical Computer Science",
volume = "105",
number = "2",
pages = "217 - 273",
year = "1992",
doi = "http://dx.doi.org/10.1016/0304-3975(92)90302-V",
}

@article{goguen1994oxford,
  title={An Oxford survey of order sorted algebra},
  author={Goguen, Joseph and Diaconescu, R{\u{a}}zvan},
  journal={Mathematical Structures in Computer Science},
  volume={4},
  number={3},
  pages={363--392},
  year={1994},
  publisher={Cambridge University Press}
}

@incollection{Goguen1991types,
 author = {Goguen, Joseph A.},
 chapter = {Types As Theories},
 title = {Topology and Category Theory in Computer Science},
 editor = {Reed, G. M. and Roscoe, A. W. and Wachter, R. F.},
 year = {1991},
 isbn = {0-19-853760-3},
 pages = {357--385},
 numpages = {29},
 url = {http://dl.acm.org/citation.cfm?id=130236.135134},
 acmid = {135134},
 publisher = {Oxford University Press, Inc.},
 address = {New York, NY, USA},
}

@book{goguen1976initial,
  title={An Initial Algebra Approach to the Specification, Correctness, and Implementation of Abstract Data Types},
  author={Goguen, J.A. and Thatcher, J.W. and Wagner, E.G.},
  series={IBM research reports},
  url={https://books.google.com/books?id=Hi1yPgAACAAJ},
  year={1976},
  publisher={IBM Research Center}
}

@article{Goguen:1977:IAS:321992.321997,
 author = {Goguen, J. A. and Thatcher, J. W. and Wagner, E. G. and Wright, J. B.},
 title = {Initial Algebra Semantics and Continuous Algebras},
 journal = {Journal of the Association for Computing Machinery},
 issue_date = {Jan. 1977},
 volume = {24},
 number = {1},
 month = jan,
 year = {1977},
 issn = {0004-5411},
 pages = {68-95},
 numpages = {28},
 url = {http://doi.acm.org/10.1145/321992.321997},
 doi = {10.1145/321992.321997},
 acmid = {321997},
 publisher = {ACM},
}

@Article{Becker1930,
author="Becker, Oskar",
title="Zur logik der modalit{\"a}ten",
journal="Jahrbuch f{\"u}r Philosophie und Ph{\"a}nomenologische Forschung",
year="1930",
volume="11",
pages="497-548"
}

@article{kripke1959,
author = "Kripke, Saul A.",
fjournal = "Journal of Symbolic Logic",
journal = "Journal of Symbolic Logic",
month = "03",
number = "1",
pages = "1-14",
publisher = "Association for Symbolic Logic",
title = "A Completeness Theorem in Modal Logic",
url = "http://projecteuclid.org/euclid.jsl/1183733464",
volume = "24",
year = "1959"
}

@Article{Godel1930,
author="G{\"o}del, Kurt",
title="Die Vollst{\"a}ndigkeit der Axiome des logischen Funktionenkalk{\"u}ls",
journal="Monatshefte f{\"u}r Mathematik und Physik",
year="1930",
volume="37",
number="1",
pages="349-360",
issn="1436-5081",
doi="10.1007/BF01696781",
url="http://dx.doi.org/10.1007/BF01696781"
}

@article{Godel1931,
  author = "G{\"o}del, Kurt",
  title = "{\"U}ber formal unentscheidbare S{\"a}tze der Principia Mathematica und verwandter Systeme {I}",
  journal = "Monatshefte f{\"u}r Mathematik und Physik",
  year = "1931",
  volume = "38",
  number = "1",
  pages = "173-198",
  timestamp = {2015-09-15T11:55:09.000+0200},
}

@inproceedings{stefanescu-park-yuwen-li-rosu-2016-oopsla,
    author = "\c{S}tef\u{a}nescu, Andrei and Park, Daejun and Yuwen, Shijiao and Li, Yilong and Ro\c{s}u, Grigore",
    publisher = "ACM",
    doi = "http://dx.doi.org/10.1145/2983990.2984027",
    title = "Semantics-Based Program Verifiers for All Languages",
    booktitle = "OOPSLA'16",
    year = "2016",
    pages = "74-91"
}

@inproceedings{serbanuta-rosu-2012-icgt,
  author    = {Traian Florin Serbanuta and
               Grigore Rosu},
  title     = {A Truly Concurrent Semantics for the K Framework Based on
               Graph Transformations},
  booktitle = {ICGT},
  year      = {2012},
  pages     = {294-310},
  ee        = {http://dx.doi.org/10.1007/978-3-642-33654-6_20},
  crossref  = {DBLP:conf/gg/2012},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/gg/2012,
  editor    = {Hartmut Ehrig and
               Gregor Engels and
               Hans-J{\"o}rg Kreowski and
               Grzegorz Rozenberg},
  title     = {Graph Transformations - 6th International Conference, ICGT
               2012, Bremen, Germany, September 24-29, 2012. Proceedings},
  booktitle = {ICGT},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {7562},
  year      = {2012},
  isbn      = {978-3-642-33653-9},
  ee        = {http://dx.doi.org/10.1007/978-3-642-33654-6},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{rosu-2015-rta,
    author = "Ro\c{s}u, Grigore",
    title = "Matching Logic -- Extended Abstract",
    series = "Leibniz International Proceedings in Informatics (LIPIcs)",
    booktitle = "RTA'15",
    year = "2015",
    month = "July",
    volume = "36",
    pages = "5-21"
}

@article{Jay:2004:PC:1034774.1034775,
 author = {Jay, C. Barry},
 title = {The Pattern Calculus},
 journal = {ACM Transactions on Programming Languages and Systems},
 volume = {26},
 number = {6},
 year = {2004},
 issn = {0164-0925},
 pages = {911-937},
 numpages = {27},
 url = {http://doi.acm.org/10.1145/1034774.1034775},
 doi = {10.1145/1034774.1034775},
 acmid = {1034775},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Constructor calculus, functional programming, generic programming, pattern calculus, pattern-matching},
}

@techreport{rosu-2014-tr,
  author   = {Grigore Ro\c{s}u},
  title    = {Matching Logic: A Logic for Structural Reasoning},
  institution = {University of Illinois},
  month       = {Jan},
  year        = {2014},
  number      = {http://hdl.handle.net/2142/47004},

  author_id         = {Grigore Rosu},
  category          = {fsl,matching_logic,K,logics,program_verification,semantics,executable_semantics},
  project_url       = {http://matching-logic.org},
  project_name      = {Matching Logic},
  hidden            = {false},
}

@inproceedings{DBLP:conf/cade/IosifRS13,
  author    = {Radu Iosif and
               Adam Rogalewicz and
               Jir\'{\i} Sim{\'a}cek},
  title     = {The Tree Width of Separation Logic with Recursive Definitions},
  booktitle = {CADE'13},
  year      = {2013},
  series    = {LNCS},
  volume    = {7898},
}

@TechReport{Brotherston-etal:TR13,
  author    = "James Brotherston and Carsten Fuhs and Nikos Gorogiannis and Juan {Navarro
  P\'erez}",
  title     = "A Decision Procedure for Satisfiability in Separation Logic with Inductive
  Predicates",
  institution = "University College London",
  number    = "RN/13/15",
  year      = 2013
}

@article{tarski1987formalization,
  title={A Formalization of Set Theory Without Variables},
  author={Tarski, A. and Givant, S.R.},
  journal={Colloquium Publications},
  volume={41},
  isbn={9780821874745},
  lccn={86022168},
  year={1987},
  publisher={American Mathematical Society}
}

@article{DBLP:journals/sLogica/FarmerG00,
  author    = {William M. Farmer and
               Joshua D. Guttman},
  title     = {A Set Theory with Support for Partial Functions},
  journal   = {Studia Logica},
  volume    = {66},
  number    = {1},
  year      = {2000},
  pages     = {59-78},
  ee        = {http://dx.doi.org/10.1023/A:1026744827863},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{z3-solver,
 author = {De Moura, Leonardo and Bj{\o}rner, Nikolaj},
 title = {{Z3: an efficient SMT solver}},
 booktitle = {TACAS'08},
 year = {2008},
 series = {LNCS},
 volume = {4963},
 pages = {337-340},
}

@inproceedings{sep-logic-csl01,
year={2001},
isbn={978-3-540-42554-0},
booktitle={CSL'01},
title={Local Reasoning about Programs that Alter Data Structures},
series={LNCS},
volume={2142},
author={O'Hearn, Peter and Reynolds, John and Yang, Hongseok},
pages={1-19},
}

@inproceedings{rosu-serbanuta-2013-k,
    author = "Rosu, Grigore and Serbanuta, Traian Florin",
    publisher = "Elsevier",
    doi = "http://dx.doi.org/10.1016/j.entcs.2014.05.002",
    title = "K Overview and SIMPLE Case Study",
    series = "ENTCS",
    booktitle = "Proceedings of International K Workshop (K'11)",
    month = "June",
    volume = "304",
    year = "2014",
    pages = "3-56"
}

@mastersthesis{guth-2013-thesis,
  author   = {Dwight Guth},
  title    = {A Formal Semantics of {Python} 3.3},
  author_id    = {Dwight Guth},
  category     = {fsl, executable_semantics, programming_languages, semantics, K},
  project_url  = {https://github.com/kframework/python-semantics},
  project_name = {Semantics},
  school = {University of Illinois at Urbana-Champaign},
  month  = {July},
  year   = {2013},
  note={\url{https://github.com/kframework/python-semantics}}
}

@manual{gappa,
title = "Gappa",
author = "Guillaume Melquiond",
note = {\url{http://gappa.gforge.inria.fr/}},
year = "2014 (accessed July 2, 2014)"
}

@article{gnu-mpfr,
 author = {Fousse, Laurent and Hanrot, Guillaume and Lef\`{e}vre, Vincent and P{\'e}lissier, Patrick and Zimmermann, Paul},
 title = {{MPFR}: A Multiple-precision Binary Floating-point Library with Correct Rounding},
 journal = {ACM Trans. Math. Softw.},
 issue_date = {June 2007},
 volume = {33},
 number = {2},
 month = jun,
 year = {2007},
 issn = {0098-3500},
 articleno = {13},
 url = {http://doi.acm.org/10.1145/1236463.1236468},
 doi = {10.1145/1236463.1236468},
 acmid = {1236468},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {IEEE 754 standard, Multiple-precision arithmetic, correct rounding, elementary function, floating-point arithmetic, portable software},
}

@techreport{stefanescu-ciobaca-moore-serbanuta-rosu-2013-tr,
    author = "\c{S}tef\u{a}nescu, Andrei and Ciob\^{a}c\u{a}, \c{S}tefan and Moore, Brandon M. and \c{S}erb\u{a}nu\c{t}\u{a}, Traian Florin and Ro\c{s}u, Grigore",
    month = "Nov",
    year = "2013",
    number = "http://hdl.handle.net/2142/46296",
    institution = "University of Illinois",
    title = "Reachability Logic in K"
}


@inproceedings{rosu-stefanescu-ciobaca-moore-2013-lics,
    author = "Grigore Ro\c{s}u and Andrei \c{S}tef\u{a}nescu and \c{S}tefan Ciob\^{a}c\u{a} and Brandon M. Moore",
    publisher = "IEEE",
    booktitle = "LICS'13",
    year = "2013",
    title = "One-Path Reachability Logic",
    pages     = {358--367},
}

@inproceedings{meredith-hills-rosu-2007-scheme,
author = {Patrick Meredith, Mark Hills, Grigore Ro\c{s}u},
title = "{An Executable Rewriting Logic Semantics of K-Scheme}",
year = {2007},
editor = {Danny Dube},
booktitle = {Proceedings of the 2007 Workshop on Scheme and Functional Programming (SCHEME'07), Technical Report DIUL-RT-0701},
publisher = {Laval University},
pages = {91-103}
}

@inproceedings{rosu-stefanescu-2012-icalp,
  author    = {Grigore Rosu and Andrei Stefanescu},
  title     = {Towards a Unified Theory of Operational and Axiomatic Semantics},
  booktitle = {Proceedings of the 39th International Colloquium on Automata, Languages and Programming (ICALP'12)},
  pages     = {351-363},
  volume    = {7392},
  series    = {LNCS},
  publisher = {Springer},
  year      = {2012},
}

@book{DBLP:books/daglib/0070910,
  author    = {Glynn Winskel},
  title     = {The formal semantics of programming languages - an introduction},
  publisher = {MIT Press},
  series    = {Foundation of computing series},
  year      = {1993},
  xxxisbn      = {978-0-262-23169-5},
  pages     = {I-XVIII, 1-361},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/csl/OHearnRY01,
  author    = {Peter W. O'Hearn and
               John C. Reynolds and
               Hongseok Yang},
  title     = {Local Reasoning about Programs that Alter Data Structures},
  booktitle = {CSL},
  year      = {2001},
  pages     = {1-19},
  ee        = {http://dx.doi.org/10.1007/3-540-44802-0_1},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/icalp/RosuS12,
  author    = {Grigore Rosu and
               Andrei Stefanescu},
  title     = {Towards a Unified Theory of Operational and Axiomatic
               Semantics},
  booktitle = {ICALP (2)},
  year      = {2012},
  pages     = {351-363},
  series    = {LNCS},
  volume    = {7392},
  ee        = {http://dx.doi.org/10.1007/978-3-642-31585-5_33},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{rosu-stefanescu-2012-fm,
  author    = {Grigore Rosu and Andrei Stefanescu},
  title     = {From Hoare Logic to Matching Logic Reachability},
  booktitle = {FM'12},
  year      = {2012},
  pages     = {387-402},
  series    = {LNCS},
  volume    = {7436},
}

@techreport{rosu-stefanescu-2012-tr-c,
  author      = {Grigore Rosu and Andrei Stefanescu},
  institution = {Univ. of Illinois},
  title       = {Towards a Unified Theory of Operational and Axiomatic
                 Semantics -- Extended Abstract},
  number      = {\url{http://hdl.handle.net/2142/30472}},
  month       = {Feb.},
  year        = {2012},
  note        = {Submitted.},
}

@techreport{rosu-stefanescu-2012-tr-b,
  author      = {Grigore Rosu and Andrei Stefanescu},
  institution = {Univ. of Illinois},
  title       = {From {H}oare Logic to Matching Logic},
  number      = {\url{http://hdl.handle.net/2142/30471}},
  month       = {Mar.},
  year        = {2012},
  note        = {Submitted.},
}

@article{DBLP:journals/toplas/Apt81,
  author    = {Krzysztof R. Apt},
  title     = {Ten Years of {Hoare}'s Logic: {A} Survey - {P}art 1},
  journal   = {ACM Trans. Program. Lang. Syst.},
  volume    = {3},
  number    = {4},
  year      = {1981},
  pages     = {431-483},
  ee        = {http://doi.acm.org/10.1145/357146.357150},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@article{DBLP:journals/siamcomp/Cook78,
  author    = {Stephen A. Cook},
  title     = {Soundness and Completeness of an Axiom System for Program
               Verification},
  journal   = {SIAM J. Comput.},
  volume    = {7},
  number    = {1},
  year      = {1978},
  pages     = {70-90},
  ee        = {http://dx.doi.org/10.1137/0207005},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@techreport{rosu-stefanescu-2012-tr,
  author      = {Grigore Rosu and Andrei Stefanescu},
  institution = {Univ. of Illinois},
  title       = {Towards a Unified Theory of Operational and Axiomatic Semantics},
  number      = {\url{http://hdl.handle.net/2142/29946}},
  month       = {Feb.},
  year        = {2012},
  note        = {Submitted.},
}


@book{hoare-jifeng-1998,
  author    = {C. A. R. Hoare and He Jifeng},
  title     = {Unifying Theories of Programming},
  publisher = {Prentice Hall},
  year      = {1998},
  isbn      = {0-13-458761-8}
}

@article{DBLP:journals/entcs/SasseM07,
  author    = {Ralf Sasse and
               Jos{\'e} Meseguer},
  title     = {Java+{ITP}: A Verification Tool Based on {Hoare} Logic and
               Algebraic Semantics},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {176},
  number    = {4},
  year      = {2007},
  pages     = {29-46},
  ee        = {http://dx.doi.org/10.1016/j.entcs.2007.06.006},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/tphol/LiuM04,
  author    = {Hanbing Liu and
               J. Strother Moore},
  title     = {Java Program Verification via a {JVM} Deep Embedding in {ACL2}},
  booktitle = {TPHOLs},
  year      = {2004},
  pages     = {184-200},
  volume    = {3223},
  series    = {LNCS},
  isbn      = {3-540-23017-3},
  ee        = {http://dx.doi.org/10.1007/978-3-540-30142-4_14},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@book{raise-1995,
author = {
 Chris George and
 Anne E. Haxthausen and
 Steven Hughes and
 Robert Milne and
 Søren Prehn and
 Jan Storbank Pedersen
},
title= {The {RAISE} Development Method},
publisher = {BCS Practitioner Series, Prentice Hall},
year= 1995,
isbn={0-13-752700-4}
}

@article{DBLP:journals/jlp/Jacobs04,
  author    = {Bart Jacobs},
  title     = {Weakest pre-condition reasoning for {Java} programs with {JML}
               annotations},
  journal   = {The Journal of Logic and Algebraic Programming},
  volume    = {58},
  number    = {1-2},
  year      = {2004},
  pages     = {61-88},
  ee        = {http://dx.doi.org/10.1016/j.jlap.2003.07.005},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@techreport{rosu-ellison-schulte-2009-tr,
author={Grigore Ro\c{s}u and Chucky Ellison and Wolfram Schulte},
title={From Rewriting Logic Executable Semantics to Matching Logic Program Verification},
number={http://hdl.handle.net/2142/13159},
institution={University of Illinois},
year={2009},
month={July},
url={http://hdl.handle.net/2142/13159}
}

@techreport{rosu-stefanescu-2011-tr,
  author      = {Grigore Rosu and Andrei Stefanescu},
  institution = {University of Illinois},
  number      = {http://hdl.handle.net/2142/28357},
  title       = {Matching Logic Rewriting: Unifying Operational and Axiomatic
                 Semantics in a Practical and Generic Framework},
  month       = "November",
  year        = "2011",
}

@article{Nipkow-FAC98,
  author  = {Tobias Nipkow},
  title   = {Winskel is (almost) Right: Towards a Mechanized Semantics Textbook},
  journal = {Formal Aspects of Computing},
  volume  = 10,
  pages   = {171-186},
  year    = 1998
}

@inproceedings{DBLP:conf/pldi/MollerS01,
  author    = {Anders M{\o}ller and
               Michael I. Schwartzbach},
  title     = {The Pointer Assertion Logic Engine},
  booktitle = {PLDI},
  year      = {2001},
  pages     = {221-231},
  ee        = {http://doi.acm.org/10.1145/378795.378851},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/tcs/BerryB92,
  author    = {G{\'e}rard Berry and
               G{\'e}rard Boudol},
  title     = {The Chemical Abstract Machine},
  journal   = {Th. Comp. Sci.},
  volume    = {96},
  number    = {1},
  year      = {1992},
  pages     = {217-248},
  ee        = {http://dx.doi.org/10.1016/0304-3975(92)90185-I},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/siamcomp/BergstraT83,
  author    = {Jan A. Bergstra and
               J. V. Tucker},
  title     = {Initial and Final Algebra Semantics for Data Type Specifications:
               Two Characterization Theorems},
  journal   = {SIAM J. Comput.},
  volume    = {12},
  number    = {2},
  year      = {1983},
  pages     = {366-387},
  ee        = {http://dx.doi.org/10.1137/0212024},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{bt95,
title = "Equational specifications, complete term rewriting systems, and
  computable and semicomputable algebras",
author = "Jan Bergstra and John Tucker",
journal = "Journal of the Association for Computing Machinery",
volume = 42,
number = 6,
pages = "1194--1230",
year = 1995}

@article{DBLP:journals/cacm/BarnettFLMSV11,
  author    = {Mike Barnett and
               Manuel F{\"a}hndrich and
               K. Rustan M. Leino and
               Peter M{\"u}ller and
               Wolfram Schulte and
               Herman Venter},
  title     = {Specification and verification: the {Spec\#} experience},
  journal   = {Commun. ACM},
  volume    = {54},
  number    = {6},
  year      = {2011},
  pages     = {81-91},
  ee        = {http://doi.acm.org/10.1145/1953122.1953145},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/pldi/ZeeKR09,
  author    = {Karen Zee and
               Viktor Kuncak and
               Martin C. Rinard},
  title     = {An integrated proof language for imperative programs},
  booktitle = {PLDI},
  year      = {2009},
  pages     = {338-351},
  ee        = {http://doi.acm.org/10.1145/1542476.1542514},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/lpar/Leino10,
  author    = {K. Rustan M. Leino},
  title     = {Dafny: An Automatic Program Verifier for Functional Correctness},
  booktitle = {LPAR},
  year      = {2010},
  pages     = {348-370},
  ee        = {http://dx.doi.org/10.1007/978-3-642-17511-4_20},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/popl/MagillTLT10,
  author    = {Stephen Magill and
               Ming-Hsien Tsai and
               Peter Lee and
               Yih-Kuen Tsay},
  title     = {Automatic numeric abstractions for heap-manipulating programs},
  booktitle = {POPL},
  year      = {2010},
  pages     = {211-222},
  ee        = {http://doi.acm.org/10.1145/1706299.1706326},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/vmcai/NguyenDQC07,
  author    = {Huu Hai Nguyen and
               Cristina David and
               Shengchao Qin and
               Wei-Ngan Chin},
  title     = {Automated Verification of Shape and Size Properties Via
               Separation Logic},
  booktitle = {VMCAI},
  year      = {2007},
  pages     = {251-266},
  ee        = {http://dx.doi.org/10.1007/978-3-540-69738-1_18},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/popl/ChangR08,
  author    = {Bor-Yuh Evan Chang and
               Xavier Rival},
  title     = {Relational inductive shape analysis},
  booktitle = {POPL},
  year      = {2008},
  pages     = {247-260},
  ee        = {http://doi.acm.org/10.1145/1328438.1328469},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/fmco/BerdineCO05,
  author    = {Josh Berdine and
               Cristiano Calcagno and
               Peter W. O'Hearn},
  title     = {Smallfoot: Modular Automatic Assertion Checking with Separation
               Logic},
  booktitle = {FMCO},
  year      = {2005},
  pages     = {115-137},
  ee        = {http://dx.doi.org/10.1007/11804192_6},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/cav/BerdineCI11,
  author    = {Josh Berdine and
               Byron Cook and
               Samin Ishtiaq},
  title     = {SLAyer: Memory Safety for Systems-Level Code},
  booktitle = {CAV},
  year      = {2011},
  pages     = {178-183},
  ee        = {http://dx.doi.org/10.1007/978-3-642-22110-1_15},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/nfm/JacobsSPVPP11,
  author    = {Bart Jacobs and
               Jan Smans and
               Pieter Philippaerts and
               Fr{\'e}d{\'e}ric Vogels and
               Willem Penninckx and
               Frank Piessens},
  title     = {VeriFast: A Powerful, Sound, Predictable, Fast Verifier
               for C and Java},
  booktitle = {NASA Formal Methods},
  year      = {2011},
  pages     = {41-55},
  ee        = {http://dx.doi.org/10.1007/978-3-642-20398-5_4},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{ellison-rosu-2012-popl,
  author    = "Chucky Ellison and Grigore Rosu",
  title     = {An executable formal semantics of {C} with applications},
  booktitle = {POPL},
  year      = {2012},
  pages     = {533-544},
  publisher = {ACM},
  ee        = {http://doi.acm.org/10.1145/2103656.2103719},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{findler-aplas-2011,
author = "Casey Klein and Jay McCarthy and Steven Jaconette and Robert Bruce Findler ",
booktitle = "APLAS",
title = "A Semantics for Context-Sensitive Reduction Semantics",
year = "2011",
note = "To appear."
}

@inproceedings{DBLP:conf/rta/MatthewsFFF04,
  author    = {Jacob Matthews and
               Robert Bruce Findler and
               Matthew Flatt and
               Matthias Felleisen},
  title     = {A Visual Environment for Developing Context-Sensitive Term
               Rewriting Systems},
  booktitle = {RTA},
  year      = {2004},
  pages     = {301-311},
  ee        = {http://dx.doi.org/10.1007/978-3-540-25979-4_21},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@book{DBLP:books/daglib/0023092,
  author    = {Matthias Felleisen and
               Robert Bruce Findler and
               Matthew Flatt},
  title     = {Semantics Engineering with PLT Redex},
  publisher = {MIT},
  year      = {2009},
  xxxisbn      = {978-0-262-06275-6},
  pages     = {I-XII, 1-502},
  ee        = {http://mitpress.mit.edu/catalog/item/default.asp?ttype=2{\&}tid=11885},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/pldi/Chlipala11,
  author    = {Adam Chlipala},
  title     = {Mostly-automated verification of low-level programs in computational
               separation logic},
  booktitle = {PLDI},
  year      = {2011},
  pages     = {234-245},
  ee        = {http://doi.acm.org/10.1145/1993498.1993526},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/esop/Appel11,
  author    = {Andrew W. Appel},
  title     = {Verified Software Toolchain},
  booktitle = {ESOP'11},
  year      = {2011},
  pages     = {1-17},
  volume    = {6602},
  series    = {LNCS},
  xxxisbn      = {978-3-642-19717-8},
  ee        = {http://dx.doi.org/10.1007/978-3-642-19718-5_1},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{joel-2014-fossacs,
  author    = {Timos Antonopoulos and
               Nikos Gorogiannis and
               Christoph Haase and
               Max I. Kanovich and
               Jo{\"{e}}l Ouaknine},
  title     = {Foundations for Decision Problems in Separation Logic with General
               Inductive Predicates},
  booktitle = {FOSSACS'14},
  pages     = {411-425},
  year      = {2014},
  series = {LNCS},
  volume = {8412},
}

@article{DBLP:journals/jar/BlazyL09,
  author    = {Sandrine Blazy and
               Xavier Leroy},
  title     = {Mechanized Semantics for the {Clight} Subset of the {C}
               Language},
  journal   = {J. Autom. Reasoning},
  volume    = {43},
  number    = {3},
  year      = {2009},
  pages     = {263-288},
  ee        = {http://dx.doi.org/10.1007/s10817-009-9148-3},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/esop/HoborAN08,
  author    = {Aquinas Hobor and
               Andrew W. Appel and
               Francesco Zappa Nardelli},
  title     = {Oracle Semantics for Concurrent Separation Logic},
  booktitle = {ESOP},
  year      = {2008},
  pages     = {353-367},
  volume    = {4960},
  series    = {LNCS},
  ee        = {http://dx.doi.org/10.1007/978-3-540-78739-6_27},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/wadt/BergHJP99,
  author    = {Joachim van den Berg and
               Marieke Huisman and
               Bart Jacobs and
               Erik Poll},
  title     = {A Type-Theoretic Memory Model for Verification of Sequential
               Java Programs},
  booktitle = {WADT},
  year      = {1999},
  pages     = {1-21},
  ee        = {http://dx.doi.org/10.1007/978-3-540-44616-3_1},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{rosu-lucanu-2009-calco,
  author    = {Grigore Rosu and
               Dorel Lucanu},
  title     = {Circular Coinduction: A Proof Theoretical Foundation},
  booktitle = {CALCO},
  year      = {2009},
  pages     = {127-144},
  volume    = {5728},
  series    = {LNCS},
  isbn      = {978-3-642-03740-5},
  ee        = {http://dx.doi.org/10.1007/978-3-642-03741-2_10},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/sas/LoginovRS06,
  author    = {Alexey Loginov and
               Thomas W. Reps and
               Mooly Sagiv},
  title     = {Automated Verification of the {Deutsch-Schorr-Waite}
               Tree-Traversal Algorithm},
  booktitle = {SAS},
  year      = {2006},
}

@article{macqueen-sannella-85,
  author    = {David B. MacQueen and
               Donald Sannella},
  title     = {Completeness of Proof Systems for Equational Specifications},
  journal   = {IEEE Trans. Software Eng.},
  volume    = {11},
  number    = {5},
  year      = {1985},
  pages     = {454-461},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{bergstra-tucker-83,
  author    = {Jan A. Bergstra and J. V. Tucker},
  title     = {Initial and Final Algebra Semantics for Data Type Specifications:
               Two Characterization Theorems},
  journal   = {SIAM J. Comput.},
  volume    = {12},
  number    = {2},
  year      = {1983},
  pages     = {366-387},
  ee        = {http://dx.doi.org/10.1137/0212024},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@book{mosses-casl,
  author    = {Peter D. Mosses},
  title     = {{CASL} Reference Manual},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {2960},
  year      = {2004},
  ee        = {http://dx.doi.org/10.1007/b96103},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{rosu-stefanescu-2011-nier-icse,
  author    = {Grigore Rosu and
               Andrei Stefanescu},
  title     = {Matching logic: a new program verification approach ({NIER}
               track)},
  booktitle = {ICSE-NIER'11},
  year      = {2011},
  pages     = {868-871},
  publisher = "ACM",
  ee        = {http://doi.acm.org/10.1145/1985793.1985928},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@techreport{ellison-rosu-2010-tr,
  author = "Chucky Ellison and Grigore Ro{\c s}u",
  institution={University of Illinois},
  number={http://hdl.handle.net/2142/17414},
  title = "A Formal Semantics of {C} with Applications",
  month = "November",
  year = "2010",
}

@inproceedings{meredith-katelman-meseguer-rosu-2010-memocode,
  author={Patrick O'Neil Meredith and Michael Katelman and Jos{\'e} Meseguer and Grigore Ro\c{s}u},
  title={A Formal Executable Semantics of {V}erilog},
  booktitle={Eighth ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'10)},
  year={2010},
  publisher={IEEE},
  pages={179-188},
  doi={doi:10.1109/MEMCOD.2010.555863}
}

@inproceedings{rosu-ellison-schulte-2010-amast,
  author    = {Grigore Rosu and
               Chucky Ellison and
               Wolfram Schulte},
  title     = {Matching Logic: An Alternative to {Hoare/Floyd} Logic},
  booktitle = {AMAST'10},
  year      = {2010},
  pages     = {142-162},
  volume    = {6486},
  series    = {LNCS},
  xxxisbn      = {978-3-642-17795-8},
  ee        = {http://dx.doi.org/10.1007/978-3-642-17796-5_9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/kbse/PavlovicS01,
  author    = {Dusko Pavlovic and
               Douglas R. Smith},
  title     = {Composition and Refinement of Behavioral Specifications},
  booktitle = {ASE},
  year      = {2001},
  pages     = {157-165},
  ee        = {http://doi.ieeecomputersociety.org/10.1109/ASE.2001.989801},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{rosu-schulte-serbanuta-2009-rv,
  author    = {Grigore Rosu and
               Wolfram Schulte and
               Traian-Florin Serbanuta},
  title     = {Runtime Verification of {C} Memory Safety},
  booktitle = {RV},
  year      = {2009},
  pages     = {132-151},
  ee        = {http://dx.doi.org/10.1007/978-3-642-04694-0_10},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@techreport{rosu-ellison-schulte-2009-tr,
  author={Grigore Ro\c{s}u and Chucky Ellison and Wolfram Schulte},
  title={From Rewriting Logic Executable Semantics to Matching Logic Program Verification},
  number={\url{http://hdl.handle.net/2142/13159}},
  institution={UIUC},
  year={2009},
  xxxmonth={July},
  xxxurl={http://hdl.handle.net/2142/13159}
}

@techreport{rosu-schulte-2009-tr,
  author={G. Ro\c{s}u and W. Schulte},
  title={Matching Logic\mdash {Extended} Report},
  number={UIUCDCS-R-2009-3026},
  institution={University of Illinois},
  year=2009,
  xxxmonth={January},
}


@incollection{iobj,
  author = "J. Goguen and T. Winkler and J. Meseguer and K. Futatsugi and J.-P. Jouannaud",
  title = "Introducing {OBJ}",
  booktitle = "Software Engineering with {OBJ}: {A}lgebraic specification in action",
  year = "2000", pages = "3-167",
  publisher = "Kluwer"
}

@book{mosses_caslReferenceManual_2004,
  added-at = {2013-02-28T11:13:35.000+0100},
  author = {Mosses, Peter D.},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  biburl = {https://www.bibsonomy.org/bibtex/23c879674b6b2689132aa8fdbff6d7773/fritzsolms},
  ee = {http://dx.doi.org/10.1007/b96103},
  interhash = {7c10941ddd3373edcfb6d75c040d1101},
  intrahash = {3c879674b6b2689132aa8fdbff6d7773},
  isbn = {3-540-21301-5},
  keywords = {imported},
  publisher = {Springer},
  series = {LNCS},
  timestamp = {2013-02-28T11:14:21.000+0100},
  title = {CASL Reference Manual, The Complete Documentation of the
               Common Algebraic Specification Language},
  volume = 2960,
  year = 2004
}

@article{serbanuta-rosu-meseguer-2007-ic,
  author    = {Traian-Florin Serbanuta and
               Grigore Rosu and
               Jos{\'e} Meseguer},
  title     = {A rewriting logic approach to operational semantics},
  journal   = {Inf. Comput.},
  volume    = {207},
  number    = {2},
  year      = {2009},
  pages     = {305-340},
  ee        = {http://dx.doi.org/10.1016/j.ic.2008.03.026},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@article{sabry-felleisen-93,
  author    = {Amr Sabry and
               Matthias Felleisen},
  title     = {Reasoning about Programs in Continuation-Passing Style},
  journal   = {Lisp and Symbolic Computation},
  volume    = {6},
  number    = {3-4},
  year      = {1993},
  pages     = {289-360},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{landin-64,
  author = {P.J. Landin},
  title = {The Mechanical evaluation of Expressions},
  journal = {The Computer Journal},
  year = {1964},
  volume = {6},
  number = {4},
  pages = {308-320}
}

@techreport{danvy04refocusing,
  author = 	 "O. Danvy and L.R. Nielsen",
  title = 	 "Refocusing in Reduction Semantics",
  institution =  "BRICS",
  year = 	 {2004},
  xxxtype = 	 "RS",
  number = 	 "RS-04-26",
  xxxaddress = 	 " DAIMI, Department of Computer Science,    University of Aarhus, Aarhus, Denmark",
  xxxmonth = 	 "November"
}

@article{reduction-compilation,
  author    = {Yong Xiao and
               Zena M. Ariola and
               Michel Mauny},
  title     = {From Syntactic Theories to Interpreters: A Specification
               Language and Its Compilation},
  journal   = {The Computing Research Repository (CoRR)},
  volume    = {cs.PL/0009030},
  month = {September},
  year      = {2000},
  ee        = {http://arxiv.org/abs/cs.PL/0009030},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{abadi-cardelli-curien-levy,
  author    = {Mart\'{\i}n Abadi and
               Luca Cardelli and
               Pierre-Louis Curien and
               Jean-Jacques L{\'e}vy},
 title = {Explicit substitutions},
 booktitle = {POPL'90: Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
 year = {1990},
 isbn = {0-89791-343-4},
 pages = {31-46},
 location = {San Francisco, California, United States},
 doi = {http://doi.acm.org/10.1145/96709.96712},
 xxxpublisher = {ACM Press},
 address = {New York, NY, USA},
}

@inproceedings{qapl05,
  author    = {Gul A. Agha and
               Jos{\'e} Meseguer and
               Koushik Sen},
  title     = {{PMaude}: Rewrite-based Specification Language for Probabilistic
               Object Systems},
  series   = {Electronic Notes in Theoretical Computer Science},
  volume    = {153},
  xxxnumber	= {2},
  year      = {2006},
  booktitle = {3rd Workshop on Quantitative Aspects of Programming Languages (QAPL 05)},
  pages     = {213-239},
  ee        = {http://dx.doi.org/10.1016/j.entcs.2005.10.040},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{ahrendt-roth-sasse,
  author    = {Wolfgang Ahrendt and
               Andreas Roth and
               Ralf Sasse},
  title     = {Automatic Validation of Transformation Rules for Java Verification
               Against a Rewriting Semantics},
  year      = {2005},
  pages     = {412-426},
  ee        = {http://dx.doi.org/10.1007/11591191_29},
  editor    = {Geoff Sutcliffe and
               Andrei Voronkov},
  booktitle     = {Logic for Programming, Artificial Intelligence, and Reasoning,
               12th International Conference, LPAR 2005, Montego Bay, Jamaica,
               December 2-6, 2005, Proceedings},
  xxxpublisher = {Springer},
  series    = {LNCS},
  volume    = {3835},
   bibsource = {DBLP, http://dblp.uni-trier.de}
}

#@proceedings{DBLP:conf/lpar/2005,
  editor    = {Geoff Sutcliffe and
               Andrei Voronkov},
  title     = {Logic for Programming, Artificial Intelligence, and Reasoning,
               12th International Conference, LPAR 2005, Montego Bay, Jamaica,
               December 2-6, 2005, Proceedings},
  booktitle = {LPAR},
  xxxpublisher = {Springer},
  series    = {LNCS},
  volume    = {3835},
  year      = {2005},
  isbn      = {3-540-30553-X},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{turki-meseguer-07,
  author    = {Musab AlTurki and
               Jos{\'e} Meseguer},
  title     = {Real-time rewriting semantics of orc},
  editor    = {Michael Leuschel and
               Andreas Podelski},
  booktitle     = {Proceedings of the 9th International ACM SIGPLAN Conference
               on Principles and Practice of Declarative Programming, July
               14-16, 2007, Wroclaw, Poland},
  year      = {2007},
  xxxpublisher = {ACM Press},
   pages     = {131-142},
  ee        = {http://doi.acm.org/10.1145/1273920.1273938},
  crossref  = {DBLP:conf/ppdp/2007},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

//@proceedings{DBLP:conf/ppdp/2007,
  editor    = {Michael Leuschel and
               Andreas Podelski},
  title     = {Proceedings of the 9th International ACM SIGPLAN Conference
               on Principles and Practice of Declarative Programming, July
               14-16, 2007, Wroclaw, Poland},
  booktitle = {PPDP},
  xxxpublisher = {ACM},
  year      = {2007},
  isbn      = {978-1-59593-769-8},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}



@MastersThesis{musab-msc,
   author = 	 {Musab Al-Turki},
   title = 	 {A rewriting logic approach to the semantics of {Orc}},
   school = 	 {Department of COmputer Science, University of Illinois at Urbana-Champaign},
   year = 	 {2005},
    month = 	 {December}
}

@ARTICLE{gamma,
  author    = {Jean-Pierre Ban{\^a}tre and
               Daniel Le M{\'e}tayer},
  title     = {The {GAMMA} Model and Its Discipline of Programming},
  journal   = {Science of Computer Programming},
  volume    = {15},
  number    = {1},
  year      = {1990},
  pages     = {55-77},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{lescanne96,
  author    = {Zine-El-Abidine Benaissa and
               Daniel Briaud and
               Pierre Lescanne and
               Jocelyne Rouyer-Degli},
  title     = {$\lambda-\nu$, A Calculus of Explicit Substitutions which Preserves Strong Normalisation},
  journal   = {The Journal of Functional Programming},
  volume    = {6},
  number    = {5},
  year      = {1996},
  pages     = {699-722},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@ARTICLE{cham-tcs,
  author    = {G. Berry and
               G. Boudol},
  title     = {The Chemical Abstract Machine},
  journal   = {Theoretical Computer Science},
  volume    = {96},
  number    = {1},
  year      = {1992},
  pages     = {217-248},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@manual{elan-fsh,
  title        = {{\sf ELAN} V 3.4 User Manual},
  author       = {Borovansk\'y, Peter and Cirstea, Horatiu and Dubois, Hubert and Kirchner, Claude and Kirchner, H\'el\`ene and Moreau, Pierre-Etienne and Ringeissen, Christophe and Vittek, Marian},
  organization = {LORIA},
  address      = {Nancy (France)},
  edition      = {fourth},
  month        = {January},
  year         = {2000},
}

@ARTICLE{elan-tcs,
  author    = {Peter Borovansk{\'y} and
               Claude Kirchner and
               H{\'e}l{\`e}ne Kirchner and
               Pierre-Etienne Moreau},
  title     = {{\sf ELAN} from a rewriting logic point of view},
  journal   = {Theoretical Computer Science},
  volume    = {285},
  number    = {2},
  year      = {2002},
  pages     = {155-185},
  ee        = {http://dx.doi.org/10.1016/S0304-3975(01)00358-9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{Centaur,
 author    = {Patrick Borras and
               Dominique Cl{\'e}ment and
               Th. Despeyroux and
               Janet Incerpi and
               Gilles Kahn and
               Bernard Lang and
               V. Pascual},
  title     = {{CENTAUR}: The System},
  booktitle = {Software Development Environments (SDE)},
  year      = {1988},
  pages     = {14-24},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@PHDTHESIS{braga-thesis,
	AUTHOR = {Christiano Braga},
	TITLE = {Rewriting Logic as a Semantic Framework for
                  Modular Structural Operational Semantics},
	SCHOOL = {Departamento de Inform\'{a}tica, Pontificia
                  Universidade Cat\'{o}lica de Rio de Janeiro, Brasil},
	YEAR = {2001}
}

@inproceedings{meseguer-braga-wrla,
  author    = {Christiano Braga and
               Jos{\'e} Meseguer},
  title     = {Modular Rewriting Semantics in Practice},
  volume    = {117},
  year      = {2005},
  pages     = {393-416},
  booktitle = "Proceedings of the Fifth International Workshop on Rewriting Logic and Its Applications (WRLA 2004)",
  series   = {Electronic Notes in Theoretical Computer Science},
  xxxpublisher = "Elsevier",
  ee        = {http://dx.doi.org/10.1016/j.entcs.2004.06.019},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{broy-et-al87-fsh,
  author    = {Manfred Broy and
               Martin Wirsing and
               Peter Pepper},
  title     = {On the Algebraic Definition of Programming Languages},
  journal   = {ACM Transactions on Programming Languages and Systems (TOPLAS)},
  volume    = {9},
  number    = {1},
  year      = {1987},
  pages     = {54-99},
  ee        = {http://doi.acm.org/10.1145/9758.10501},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{bruni-meseguer,
  author    = {Roberto Bruni and
               Jos{\'e} Meseguer},
  title     = {Semantic foundations for generalized rewrite theories},
  journal   = {Theoretical Computer Science},
  volume    = {360},
  number    = {1-3},
  year      = {2006},
  pages     = {386-414},
  ee        = {http://dx.doi.org/10.1016/j.tcs.2006.04.012},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@MastersThesis{chalub-mscthesis,
   author = 	 {Fabricio Chalub},
   title = 	 {An Implementation of {Modular} {SOS} in {Maude}},
   school = 	 {Universidade Federal Fluminense},
   year = 	 {2005},
   month = 	 {May},
   note = 	 {\verb|http://www.ic.uff.br/~frosario/dissertation.pdf|},
}

@article{braga-cml,
  author    = {Fabricio Chalub and
               Christiano Braga},
  title     = {A Modular Rewriting Semantics for {CML}},
  journal   = {The Journal of Universal Computer Science},
  volume    = {10},
  number    = {7},
  year      = {2004},
  pages     = {789-807},
  ee        = {http://www.jucs.org/jucs_10_7/a_modular_rewriting_semantics},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{braga-msos,
title = "Maude {MSOS} Tool",
author = "Fabricio Chalub and Christiano Braga",
editor = {Grit Denker and Carolyn Talcott},
booktitle = {Proceedings of the Sixth International Workshop on Rewriting Logic and its Applications (WRLA 2006)},
xxxpublisher = "Elsevier",
series = "Electronic Notes in Theoretical Computer Science",
volume = {176(4)},
year = {2007},
pages= {133-146},
}

@misc{RLS-java14,
  author =       {Feng Chen and Grigore Ro\c{s}u},
  title =        "Rewriting Logic Semantics of {Java} 1.4",
  year = {2004},
  note =         {\url{http://fsl.cs.uiuc.edu/index.php/Rewriting_Logic_Semantics_of_Java}}
}

@inproceedings{rosu-PC-2,
  author    = {Feng Chen and
               Grigore Ro\c{s}u and
               Ram Prasad Venkatesan},
  title     = {Rule-Based Analysis of Dimensional Safety},
  year      = {2003},
  pages     = {197-207},
  ee        = {http://link.springer.de/link/service/series/0558/bibs/2706/27060197.htm},
  editor    = {Robert Nieuwenhuis},
  booktitle     = {Rewriting Techniques and Applications, 14th International
               Conference, RTA 2003, Valencia, Spain, June 9-11, 2003,
               Proceedings},
  xxxpublisher = {Springer},
  series    = {LNCS},
  volume    = {2706},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

#@proceedings{DBLP:conf/rta/2003,
  editor    = {Robert Nieuwenhuis},
  title     = {Rewriting Techniques and Applications, 14th International
               Conference, RTA 2003, Valencia, Spain, June 9-11, 2003,
               Proceedings},
  booktitle = {RTA},
  xxxpublisher = {Springer},
  series    = {LNCS},
  volume    = {2706},
  year      = {2003},
  isbn      = {3-540-40254-3},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{clavel-et-al99a,
  author    = {Manuel Clavel and
               Francisco Dur{\'a}n and
               Steven Eker and
               Patrick Lincoln and
               Narciso Mart\'{\i}-Oliet and
               Jos{\'e} Meseguer and
               Jose F. Quesada},
  title     = {Maude: specification and programming in rewriting logic},
  journal   = {Theoretical Computer Science},
  volume    = {285},
  number    = {2},
  year      = {2002},
  pages     = {187-243},
  ee        = {http://dx.doi.org/10.1016/S0304-3975(01)00359-0},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@BOOK{maude-book,
	AUTHOR = {M. Clavel and F. Dur\'an and S. Eker and J. Meseguer and
                  P. Lincoln and N. Mart\'{\i}-Oliet and C. Talcott},
	TITLE = {All About Maude},
	volume = {4350},
	series = {LNCS},
	publisher = {Springer},
    YEAR = {2007},
}

@inproceedings{asip-prole05,
  author =       {Manuel Clavel and Juan Santa-Cruz},
  title =        {{ASIP + ITP}: A verification tool based on algebraic
                     semantics},
  booktitle = {PROLE 2005: V Jornadas sobre Programación y Lenguajes},
  pages = {149-158},
  year = 2005,
  xxxpublisher = {Thomson},
}

@incollection(kahn-natural,
title = "Natural semantics on the computer",
author = "Dominique Cl{\'e}ment and Jo{\"e}lle Despeyroux and Laurent Hascoet and Gilles Kahn",
booktitle = "Proceedings of the France-Japan AI and CS Symposium",
editor = "Kazuhiru Fuchi and Maurice Nivat",
pages = "49-89",
publisher = "ICOT, Japan",
note = "Also, Information Processing Society of Japan, Technical Memorandum
  PL-86-6 and Rapport de recherche \#0416, INRIA",
year = 1986)

@article{amorim-rosu05,
  author    = {Marcelo d'Amorim and
               Grigore Ro\c{s}u},
  title     = {An Equational Specification for the {Scheme} Language},
  journal   = {The Journal of Universal Computer Science},
  volume    = {11},
  number    = {7},
  year      = {2005},
  pages     = {1327-1348},
  ee        = {http://www.jucs.org/jucs_11_7/an_equational_specification_for},
  bibsource = {DBLP, http://dblp.uni-trier.de},
 note = "Selected papers from the 9th Brazilian Symposium on Programming
 Languages (SBLP'05).  Also Technical Report No. UIUCDCS-R-2005-2567,
  April 2005"
}

@book{caferep98,
  author =       {R{\u{a}}zvan Diaconescu and Kokichi Futatsugi},
  title =        {{CafeOBJ} Report. The Language, Proof Techniques, and
                  Methodologies for Object-Oriented Algebraic
                  Specification},
  year =         1998,
  publisher =    {World Scientific},
  series =       {AMAST Series in Computing},
  volume =       6
}

@INPROCEEDINGS{maude-strats06,
  author = 	 {Steven Eker
              and Narcis Mart\'{\i}-Oliet
	      and Jos{\`e} Meseguer
	      and Albert Verdejo},
  title = 	 {Deduction, Strategies, and Rewriting},
	BOOKTITLE = {Proceedings of the 6th International Workshop on Strategies in Automated Deduction (STRATEGIES 2006)},
       EDITOR = {M. Archer, T. Boy de la Tour and C. Muñoz },
        PAGES = {3-25},
	volume = {174(11)},
        YEAR = {2007},
	series = {Electronic Notes in Theoretical Computer Science},
        xxxpublisher = {Elsevier},
}

@PhDThesis{farzan-phd,
  author =       {Azadeh Farzan},
  title =        {Static and dynamic formal analysis of concurrent systems and
                    languages: a semantics-based approach},
  school =       {Department of Computer Science, University of Illinois at Urbana-Champaign},
  year =         {2007}
}

@inproceedings{javafan-cav,
  author    = {A. Farzan and
               F. Chen and
               J. Meseguer and
               G. Ro\c{s}u},
  title     = {Formal Analysis of {Java} Programs in {JavaFAN}},
  year      = {2004},
  pages     = {501-505},
  booktitle     = {CAV'04},
  xxxpublisher = {Springer},
  series    = {LNCS},
  volume    = {3114}
}

#@proceedings{DBLP:conf/cav/2004,
  editor    = {Rajeev Alur and
               Doron Peled},
  title     = {Computer Aided Verification, 16th International Conference,
               CAV 2004, Boston, MA, USA, July 13-17, 2004, Proceedings},
  booktitle = {CAV},
  xxxpublisher = {Springer},
  series    = {LNCS},
  volume    = {3114},
  year      = {2004},
  isbn      = {3-540-22342-8},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@INPROCEEDINGS{farzan-meseguer-wrla06,
	AUTHOR = {A. Farzan and J. Meseguer},
	TITLE = {Partial Order Reduction for Rewriting Semantics of Programming Languages},
editor = {Grit Denker and Carolyn Talcott},
booktitle = {Proceedings of the Sixth International Workshop on Rewriting Logic and its Applications (WRLA 2006)},
xxxpublisher = "Elsevier",
series = "Electronic Notes in Theoretical Computer Science",
volume = {176(4)},
year = {2007},
pages = {61-78},
}

@inproceedings{javafan-amast,
  author    = {Azadeh Farzan and
               Jos{\'e} Meseguer and
               Grigore Ro\c{s}u},
  title     = {Formal {JVM} Code Analysis in {JavaFAN}},
  year      = {2004},
  pages     = {132-147},
  ee        = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3116{\&}spage=132},
  xxxeditor    = {Charles Rattray and
               Savi Maharaj and
               Carron Shankland},
  booktitle     = {AMAST'04},
  xxxpublisher = {Springer},
  series    = {LNCS},
  volume    = {3116},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

#@proceedings{DBLP:conf/amast/2004,
  editor    = {Charles Rattray and
               Savi Maharaj and
               Carron Shankland},
  title     = {Algebraic Methodology and Software Technology, 10th International
               Conference, AMAST 2004, Stirling, Scotland, UK, July 12-16,
               2004, Proceedings},
  booktitle = {AMAST},
  xxxpublisher = {Springer},
  series    = {LNCS},
  volume    = {3116},
  year      = {2004},
  isbn      = {3-540-22381-9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{continuations,
	Address = {Ebberup, Denmark},
	Author = {Matthias Felleisen and Daniel P. Friedman},
	Booktitle = {3rd Working Conference on the Formal Description of Programming Concepts},
	Date-Modified = {2006-07-30 22:51:21 +0200},
	Month = aug,
	Pages = {193-219},
	Title = {Control Operators, the {SECD}-Machine, and the Lambda-Calculus},
	Year = 1986}

@book{eopl,
	Address = {Cambridge, MA},
	Author = {Daniel P. Friedman and Mitchell Wand and Christopher T. Haynes},
	Date-Added = {2005-04-21 20:45:50 -0500},
	Date-Modified = {2005-04-21 20:47:38 -0500},
	Edition = {2nd},
	Isbn = {0-262-06217-8},
	publisher = {MIT Press},
	Title = {Essentials of Programming Languages},
	Url = {http://www.cs.indiana.edu/eopl/},
	Year = {2001}}

@TECHREPORT{garrido-meseguer-johnson-tech,
      AUTHOR = {A.~Garrido and J.~Meseguer and R.~Johnson},
      TITLE = {Algebraic semantics of the {C} preprocessor and correctness of its refactorings},
      INSTITUTION = {Department of Computer Science, University of Illinois at
  Urbana-Champaign},
      NUMBER = {UIUCDCS-R-2006-2688},
     MONTH = {February},
YEAR = {2006}
}

@book{goguen-malcolm96,
title = "Algebraic Semantics of Imperative Programs",
author= "Joseph Goguen and Grant Malcolm",
publisher = "MIT Press",
year = 1996}

@inproceedings{gp81,
  author    = {Joseph A. Goguen and
               Kamran Parsaye-Ghomi},
  title     = {Algebraic Denotational Semantics Using Parameterized Abstract
               Modules},
  year      = {1981},
  pages     = {292-309},
  editor    = {Josep D\'{\i}az and
               Isidro Ramos},
  booktitle     = {Formalization of Programming Concepts, International Colloquium,
               Peniscola, Spain, April 19-25, 1981, Proceedings},
  xxxpublisher = {Springer},
  series    = {LNCS},
  volume    = {107},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

#@proceedings{DBLP:conf/icfpc/1981,
  editor    = {Josep D\'{\i}az and
               Isidro Ramos},
  title     = {Formalization of Programming Concepts, International Colloquium,
               Peniscola, Spain, April 19-25, 1981, Proceedings},
  booktitle = {ICFPC},
  xxxpublisher = {Springer},
  series    = {LNCS},
  volume    = {107},
  year      = {1981},
  isbn      = {3-540-10699-5},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@incollection{ asm,
    author = "Yuri Gurevich",
    title = "Evolving Algebras 1993: {L}ipari {G}uide",
    booktitle = "Specification and Validation Methods",
    publisher = "Oxford University Press",
    editor = "Egon B{\"o}rger",
    pages = "9-37",
    year = "1994",
}

@article{har-fra,
  author    = {Robert Harper and
               Furio Honsell and
               Gordon D. Plotkin},
  title     = {A Framework for Defining Logics},
  journal   = {Journal of the ACM},
  volume    = {40},
  number    = {1},
  year      = {1993},
  pages     = {143-184},
  ee        = {http://doi.acm.org/10.1145/138027.138060},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@INPROCEEDINGS{hills-serbanuta-rosu06,
	AUTHOR = {Mark Hills and Traian Florin \c{S}erb\u{a}nu\c{t}\u{a} and Grigore Ro\c{s}u},
	TITLE = {A Rewrite Framework for Language Definitions and for Generation of Efficient Interpreters},
editor = {Grit Denker and Carolyn Talcott},
booktitle = {Proceedings of the Sixth International Workshop on Rewriting Logic and its Applications (WRLA 2006)},
xxxpublisher = "Elsevier",
series = "Electronic Notes in Theoretical Computer Science",
volume = {176(4)},
year = {2007},
pages = {215-231},
}

@INPROCEEDINGS{owe-wrla04,
  author    = {Einar Broch Johnsen and
               Olaf Owe and
               Eyvind W. Axelsen},
  title     = {A Run-Time Environment for Concurrent Objects With Asynchronous
               Method Calls},
  series   = {Electronic Notes in Theoretical Computer Science},
  volume    = {117},
  year      = {2005},
  pages     = {375-392},
  ee        = {http://dx.doi.org/10.1016/j.entcs.2004.06.012},
  bibsource = {DBLP, http://dblp.uni-trier.de},
	BOOKTITLE = {Proceedings of the Fifth International Workshop on
                Rewriting Logic and its Applications (WRLA 2004)},
        EDITOR = {N. Mart\'{\i}-Oliet},
        xxxpublisher = {Elsevier}
}

@inproceedings{natural-semantics,
  author    = {Gilles Kahn},
  title     = {Natural Semantics},
  year      = {1987},
  pages     = {22-39},
  editor    = {Franz-Josef Brandenburg and
               Guy Vidal-Naquet and
               Martin Wirsing},
  booktitle     = {STACS 87, 4th Annual Symposium on Theoretical Aspects of
               Computer Science, Passau, Germany, February 19-21, 1987,
               Proceedings},
  xxxpublisher = {Springer},
  series    = {LNCS},
  volume    = {247},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

#@proceedings{DBLP:conf/stacs/1987,
  editor    = {Franz-Josef Brandenburg and
               Guy Vidal-Naquet and
               Martin Wirsing},
  title     = {STACS 87, 4th Annual Symposium on Theoretical Aspects of
               Computer Science, Passau, Germany, February 19-21, 1987,
               Proceedings},
  booktitle = {STACS},
  xxxpublisher = {Springer},
  series    = {LNCS},
  volume    = {247},
  year      = {1987},
  isbn      = {3-540-17219-X},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@INPROCEEDINGS{katelman-meseguer-wrla06,
	AUTHOR = {M. Katelman and J. Meseguer},
	TITLE = {A Rewriting Semantics for {ABEL} with Applications to
         Hardware/Software Co-Design and Analysis},
editor = {Grit Denker and Carolyn Talcott},
booktitle = {Proceedings of the Sixth International Workshop on Rewriting Logic and its Applications (WRLA 2006)},
xxxpublisher = "Elsevier",
series = "Electronic Notes in Theoretical Computer Science",
volume = {176(4)},
year = {2007},
pages = {47-60},
}

@book{acl2jvm,
 author = "M. Kaufmann and P. Manolios and J. S. Moore",
 title = "Computer-Aided Reasoning: {ACL2} Case Studies",
 publisher = "Kluwer",
 year = "2000"
}

@inproceedings{liang-et-al-95,
 author = {Sheng Liang and Paul Hudak and Mark Jones},
 title = {Monad transformers and modular interpreters},
 booktitle = {POPL'95: Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
 year = {1995},
 isbn = {0-89791-692-1},
 pages = {333-343},
 location = {San Francisco, California, United States},
 doi = {http://doi.acm.org/10.1145/199448.199528},
 xxxpublisher = {ACM Press},
 address = {New York, NY, USA},
 }

@INCOLLECTION{rwl-fwk,
	AUTHOR = {Narciso Mart\'{\i}-Oliet and Jos\'e Meseguer},
        TITLE = {Rewriting Logic as a Logical and Semantic Framework},
        BOOKTITLE = {Handbook of Philosophical Logic, 2nd. Edition},
        EDITOR = {D. Gabbay and F. Guenthner},
        YEAR = {2002},
        PAGES = {1-87},
        publisher = {Kluwer},
        NOTE = {First published as SRI Tech. Report SRI-CSL-93-05, August 1993}
}

@ARTICLE{roadmap,
  author    = {Narciso Mart\'{\i}-Oliet and
               Jos{\'e} Meseguer},
  title     = {Rewriting logic: roadmap and bibliography},
  journal   = {Theoretical Computer Science},
  volume    = {285},
  number    = {2},
  year      = {2002},
  pages     = {121-154},
  ee        = {http://dx.doi.org/10.1016/S0304-3975(01)00357-7},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{meseguer92,
  author    = {Jos{\'e} Meseguer},
  title     = {Conditioned Rewriting Logic as a United Model of Concurrency},
  journal   = {Theor. Comput. Sci.},
  volume    = {96},
  number    = {1},
  year      = {1992},
  pages     = {73-155},
  ee        = {http://dx.doi.org/10.1016/0304-3975(92)90182-F},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@INPROCEEDINGS{concur96,
  author    = {Jos{\'e} Meseguer},
  title     = {Rewriting Logic as a Semantic Framework for Concurrency:
               a Progress Report},
  year      = {1996},
  pages     = {331-372},
  editor    = {Ugo Montanari and
               Vladimiro Sassone},
  booktitle     = {CONCUR '96, Concurrency Theory, 7th International Conference,
               Pisa, Italy, August 26-29, 1996, Proceedings},
  xxxpublisher = {Springer},
  series    = {LNCS},
  volume    = {1119},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

#@proceedings{DBLP:conf/concur/1996,
  editor    = {Ugo Montanari and
               Vladimiro Sassone},
  title     = {CONCUR '96, Concurrency Theory, 7th International Conference,
               Pisa, Italy, August 26-29, 1996, Proceedings},
  booktitle = {CONCUR},
  xxxpublisher = {Springer},
  series    = {LNCS},
  volume    = {1119},
  year      = {1996},
  isbn      = {3-540-61604-7},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@INPROCEEDINGS{tarquinia,
  author    = {Jos{\'e} Meseguer},
  title     = {Membership algebra as a logical framework for equational
               specification},
  year      = {1997},
  pages     = {18-61},
  editor    = {Francesco Parisi-Presicce},
  booktitle     = {Recent Trends in Algebraic Development Techniques, 12th
               International Workshop, WADT'97, Tarquinia, Italy, June
               1997, Selected Papers},
  xxxpublisher = {Springer},
  series    = {LNCS},
  volume    = {1376},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

#@proceedings{DBLP:conf/wadt/1997,
  editor    = {Francesco Parisi-Presicce},
  title     = {Recent Trends in Algebraic Development Techniques, 12th
               International Workshop, WADT'97, Tarquinia, Italy, June
               1997, Selected Papers},
  booktitle = {WADT},
  xxxpublisher = {Springer},
  series    = {LNCS},
  volume    = {1376},
  year      = {1997},
  isbn      = {3-540-64299-4},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@INCOLLECTION{marktoberdorf02,
	AUTHOR = {Jos\'e Meseguer},
	TITLE = {Software Specification and Verification in Rewriting Logic},
	BOOKTITLE = {Models, Algebras, and Logic of Engineering Software,
        NATO Advanced Study Institute, Marktoberdorf,
        Germany, July 30 - August 11, 2002},
	publisher = {IOS Press},
        PAGES = {133-193},
	YEAR = {2003},
	EDITOR = {M. Broy and M. Pizka}
}

@inproceedings{meseguer-braga-amast,
  author    = {Jos{\'e} Meseguer and
               Christiano Braga},
  title     = {Modular Rewriting Semantics of Programming Languages},
  year      = {2004},
  pages     = {364-378},
  ee        = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3116{\&}spage=364},
  editor    = {Charles Rattray and
               Savi Maharaj and
               Carron Shankland},
  booktitle     = {Algebraic Methodology and Software Technology, 10th International
               Conference, AMAST 2004, Stirling, Scotland, UK, July 12-16,
               2004, Proceedings},
  xxxpublisher = {Springer},
  series    = {LNCS},
  volume    = {3116},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{meseguer-rosu-2006-tcs,
  author    = {Jos{\'e} Meseguer and
               Grigore Rosu},
  title     = {The rewriting logic semantics project},
  journal   = {Theor. Comput. Sci.},
  volume    = {373},
  number    = {3},
  year      = {2007},
  pages     = {213-237},
  ee        = {http://dx.doi.org/10.1016/j.tcs.2006.12.018},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@INPROCEEDINGS{meseguer-rosu-ijcar04,
  author    = {Jos{\'e} Meseguer and
               Grigore Ro\c{s}u},
  title     = {Rewriting Logic Semantics: From Language Specifications
               to Formal Analysis Tools},
  year      = {2004},
  pages     = {1-44},
  ee        = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3097{\&}spage=1},
  editor    = {David A. Basin and
               Micha{\"e}l Rusinowitch},
  booktitle     = {Automated Reasoning - Second International Joint Conference,
               IJCAR 2004, Cork, Ireland, July 4-8, 2004, Proceedings},
  xxxpublisher = {Springer},
  series    = {LNCS},
  volume    = {3097},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

#@proceedings{DBLP:conf/cade/2004,
  editor    = {David A. Basin and
               Micha{\"e}l Rusinowitch},
  title     = {Automated Reasoning - Second International Joint Conference,
               IJCAR 2004, Cork, Ireland, July 4-8, 2004, Proceedings},
  booktitle = {IJCAR},
  xxxpublisher = {Springer},
  series    = {LNCS},
  volume    = {3097},
  year      = {2004},
  isbn      = {3-540-22345-2},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{Miller06,
  author    = {Dale Miller},
  title     = {Representing and Reasoning with Operational Semantics},
  year      = {2006},
  pages     = {4-20},
  ee        = {http://dx.doi.org/10.1007/11814771_3},
  editor    = {Ulrich Furbach and
               Natarajan Shankar},
  booktitle     = {Automated Reasoning, Third International Joint Conference,
               IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings},
  xxxpublisher = {Springer},
  series    = {LNCS},
  volume    = {4130},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

#@proceedings{DBLP:conf/cade/2006,
  editor    = {Ulrich Furbach and
               Natarajan Shankar},
  title     = {Automated Reasoning, Third International Joint Conference,
               IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings},
  booktitle = {IJCAR},
  xxxpublisher = {Springer},
  series    = {LNCS},
  volume    = {4130},
  year      = {2006},
  isbn      = {3-540-37187-7},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}



@ARTICLE{milner-nice,
  author    = {Robin Milner},
  title     = {Functions as Processes},
  journal   = {Mathematical Structures in Computer Science},
  volume    = {2},
  number    = {2},
  year      = {1992},
  pages     = {119-141},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@book{milner97,
      AUTHOR      = {Milner, Robin and Tofte, Mads and Harper, Robert and MacQueen, David},
      TITLE       = {The Definition of Standard ML (Revised)},
      YEAR        = {1997},
      publisher   = {MIT Press},
 }

@TECHREPORT{Moggi89a,
  AUTHOR = {E. Moggi},
  TITLE = {An abstract view of programming languages},
  INSTITUTION = {Edinburgh University, Department of Computer
		  Science},
  YEAR = 1989,
  MONTH = {June},
  NUMBER = {ECS-LFCS-90-113},
}

@INPROCEEDINGS{unified-action,
  author    = {Peter D. Mosses},
  title     = {Unified Algebras and Action Semantics},
  year      = {1989},
  pages     = {17-35},
  editor    = {Burkhard Monien and
               Robert Cori},
  booktitle     = {STACS 89, 6th Annual Symposium on Theoretical Aspects of
               Computer Science, Paderborn, FRG, February 16-18, 1989,
               Proceedings},
  xxxpublisher = {Springer},
  series    = {LNCS},
  volume    = {349},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

#@proceedings{DBLP:conf/stacs/1989,
  editor    = {Burkhard Monien and
               Robert Cori},
  title     = {STACS 89, 6th Annual Symposium on Theoretical Aspects of
               Computer Science, Paderborn, FRG, February 16-18, 1989,
               Proceedings},
  booktitle = {STACS},
  xxxpublisher = {Springer},
  series    = {LNCS},
  volume    = {349},
  year      = {1989},
  isbn      = {3-540-50840-6},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@incollection(mosses-denotational,
title = "Denotational Semantics",
author = "P. D.  Mosses",
booktitle = "Handbook of Theoretical Computer Science, Vol. B, Chapter 11",
year = 1990,
editor = "J. van Leeuwen",
publisher = "North-Holland")


@inproceedings{mosses-amast,
  author    = {Peter D. Mosses},
  title     = {Pragmatics of Modular {SOS}},
  year      = {2002},
  pages     = {21-40},
  ee        = {http://link.springer.de/link/service/series/0558/bibs/2422/24220021.htm},
  editor    = {H{\'e}l{\`e}ne Kirchner and
               Christophe Ringeissen},
  booktitle     = {Algebraic Methodology and Software Technology, 9th International
               Conference, AMAST 2002, Saint-Gilles-les-Bains, Reunion
               Island, France, September 9-13, 2002, Proceedings},
  xxxpublisher = {Springer},
  series    = {LNCS},
  volume    = {2422},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

#@proceedings{DBLP:conf/amast/2002,
  editor    = {H{\'e}l{\`e}ne Kirchner and
               Christophe Ringeissen},
  title     = {Algebraic Methodology and Software Technology, 9th International
               Conference, AMAST 2002, Saint-Gilles-les-Bains, Reunion
               Island, France, September 9-13, 2002, Proceedings},
  booktitle = {AMAST},
  xxxpublisher = {Springer},
  series    = {LNCS},
  volume    = {2422},
  year      = {2002},
  isbn      = {3-540-44144-1},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{mosses-jlap,
 author    = {Peter D. Mosses},
  title     = {Modular structural operational semantics},
  journal   = {Journal of Logic \& Algebraic Programming},
  volume    = {60-61},
  year      = {2004},
  pages     = {195-228},
  ee        = {http://dx.doi.org/10.1016/j.jlap.2004.03.008},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@INPROCEEDINGS{Nadathur-Miller,
  author    = {Gopalan Nadathur and
               Dale Miller},
  title     = {An Overview of {Lambda-PROLOG}},
  year      = {1988},
  pages     = {810-827},
editor = {Robert A. Kowalski, Kenneth A. Bowen},
booktitle = {Logic Programming, Proceedings of the Fifth International Conference and Symposium, Seattle, Washington, August 15-19, 1988, Proceedings},
xxxpublisher = {MIT Press},
  bibsource = {DBLP, http://dblp.uni-trier.de},
}

#@proceedings{DBLP:/conf/iclp/1988,
editor = {Robert A. Kowalski, Kenneth A. Bowen},
title = {Logic Programming, Proceedings of the Fifth International Conference and Symposium, Seattle, Washington, August 15-19, 1988, Proceedings},
booktitle = {ICLP/SLP},
xxxpublisher = {MIT Press},
year = {1988},
isbn = {0-262-61056-6},
}


@INPROCEEDINGS{real-time-maude2,
  author    = {Peter Csaba {\"O}lveczky and
               Jos{\'e} Meseguer},
  title     = {{Real-Time Maude 2.1}},
  series   = {Electronic Notes in Theoretical Computer Science},
  volume    = {117},
  year      = {2005},
  pages     = {285-314},
  ee        = {http://dx.doi.org/10.1016/j.entcs.2004.06.015},
  bibsource = {DBLP, http://dblp.uni-trier.de},
	BOOKTITLE = {Proceedings of the Fifth International Workshop on
                Rewriting Logic and its Applications (WRLA 2004)},
        EDITOR = {N. Mart\'{\i}-Oliet},
        xxxpublisher = {Elsevier}
}

@inproceedings{phe-hig,
  author    = {Frank Pfenning and
               Conal Elliott},
 title = {Higher-order abstract syntax},
 booktitle = {PLDI '88: Proceedings of the ACM SIGPLAN 1988 conference on Programming Language design and Implementation},
 year = {1988},
 isbn = {0-89791-269-1},
 pages = {199-208},
 location = {Atlanta, Georgia, United States},
 doi = {http://doi.acm.org/10.1145/53990.54010},
 xxxpublisher = {ACM Press},
 address = {New York, NY, USA},
 }

@book{pierce-book-2002,
	Author = "B. Pierce",
	title = "Types and Programming Languages",
	publisher = "MIT Press",
	year = 2002}

@article{sos,
  author    = {G.D. Plotkin},
  title     = {A structural approach to operational semantics},
  journal   = {Journal of Logic \& Algebraic Programming},
  volume    = {60-61},
  year      = {2004},
  pages     = {17-139},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  xxxnote = {Original version: University of Aarhus Technical Report DAIMI FN-19, 1981}
}

@misc{ML-website,
author={C. Ellison and G. Ro\c{s}u},
title={Matching logic website\mdash{T}ools and examples},
year=2009,
url={http://fsl.cs.uiuc.edu/ml},
xxxnote={\url{http://fsl.cs.uiuc.edu/ml}}
}

@inproceedings{reynolds-02,
  author    = {John C. Reynolds},
  title     = {Separation Logic: A Logic for Shared Mutable Data Structures},
  booktitle = {LICS'02},
  year      = {2002},
  pages     = {55-74},
  publisher = {{IEEE}},
  ee        = {http://doi.ieeecomputersociety.org/10.1109/LICS.2002.1029817},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{reynolds93discoveries,
  author    = {Reynolds, John  C.},
  title     = {The Discoveries of Continuations},
  journal   = {Lisp \& Symbolic Computation},
  volume    = {6},
  number    = {3-4},
  year      = {1993},
  pages     = {233-248},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@incollection{rosu-SYN,
  author    = {Grigore Ro\c{s}u and
               Ram Prasad Venkatesan and
               Jon Whittle and
               Laurentiu Leustean},
  title     = {Certifying Optimality of State Estimation Programs},
  year      = {2003},
  pages     = {301-314},
  ee        = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2725{\&}spage=301},
  editor    = {Warren A. Hunt Jr. and
               Fabio Somenzi},
  booktitle     = {Computer Aided Verification, 15th International Conference,
               CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {2725},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

#@proceedings{DBLP:conf/cav/2003,
  editor    = {Warren A. Hunt Jr. and
               Fabio Somenzi},
  title     = {Computer Aided Verification, 15th International Conference,
               CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings},
  booktitle = {CAV},
  xxxpublisher = {Springer},
  series    = {LNCS},
  volume    = {2725},
  year      = {2003},
  isbn      = {3-540-40524-0},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{brochenin-demri-lozes,
    abstract = {Motivated by the verification of programs with pointer variables, we introduce a temporal logic  inlMMLBox  whose underlying assertion language is the quantifier-free fragment of separation logic and the temporal logic on the top of it is the standard linear-time temporal logic LTL. We analyze the complexity of various model-checking and satisfiability problems for  inlMMLBox , considering various fragments of separation logic (including pointer arithmetic), various classes of models (with or without constant heap), and the influence of fixing the initial memory state. We provide a complete picture based on these criteria. Our main decidability result is  pspace -completeness of the satisfiability problems on the record fragment and on a classical fragment allowing pointer arithmetic.  inlMMLBox -completeness or  inlMMLBox -completeness results are established for various problems by reducing standard problems for Minsky machines, and underline the tightness of our decidability results.},
    author = {Brochenin, R\'{e}mi and Demri, St\'{e}phane and Lozes, Etienne},
    doi = {10.1016/j.apal.2009.07.004},
    issn = {01680072},
    journal = {Annals of Pure and Applied Logic},
    month = {August},
    posted-at = {2009-08-28 02:26:01},
    title = {Reasoning about sequences of memory states},
    xxxurl = {http://dx.doi.org/10.1016/j.apal.2009.07.004},
    year = {2009}
}

@INPROCEEDINGS{Calcagno01computabilityand,
    author = {Cristiano Calcagno and Hongseok Yang and Peter W. O'Hearn},
    title = {Computability and Complexity Results for a Spatial Assertion Language for Data Structures},
    booktitle = {FSTTCS'01},
    year = {2001},
    pages = {108-119},
    xxxpublisher = {Springer}
}

@inproceedings{BDL-csl08,
  	address =	{Bertinoro, Italy},
  	author =	{Brochenin, R{\'e}mi and Demri, St{\'e}phane and Lozes, {\'E}tienne},
  	xxxbooktitle =	{{P}roceedings of the 16th Annual {EACSL} Conference on Computer Science Logic ({CSL}'08)},
  	booktitle =	{CSL'08},
  	DOI =	{10.1007/978-3-540-87531-4_24},
  	editor =	{Kaminski, Michael and Martini, Simone},
  	month =	sep,
  	pages =	{323-338},
  	xxxpublisher =	{Springer},
  	series =	{LNCS},
  	title =	{On~the Almighty Wand},
  	xxxurl =	{http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDL-csl08.pdf},
  	volume =	{5213},
  	year =	{2008},
}
	

@TechReport{rosu-2007-tr-c,
author = {Grigore Ro\c{s}u},
title = "{K}:  A rewriting-based framework for computations\mdash Preliminary version",
institution = {University of Illinois, Department of Computer Science},
Number = {UIUCDCS-R-2007-2926},
Year = {2007}
}

@MASTERSTHESIS{sasse-diplom,
  author =       {Ralph Sasse},
  title =        {Taclets vs. Rewriting Logic\mdash Relating Semantics of {Java}},
  school =       {Fakult\"at f\"ur Informatik, Universit\"at Karlsruhe,
                                                       Germany},
  month = may,
  year =         2005,
  note =         {{Technical Report in Computing Science No.\ 2005-16}},
  urls  =         {http://www.ubka.uni-karlsruhe.de/cgi-bin/psview?document=ira/2005/16}
}

@article{hoare-69,
  author    = {C. A. R. Hoare},
  title     = {An Axiomatic Basis for Computer Programming},
  journal   = {Communications of the Association for Computing Machinery},
  volume    = {12},
  number    = {10},
  year      = {1969},
  pages     = {576-580},
  ee        = {http://doi.acm.org/10.1145/363235.363259},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{huisman-jacobs-2000-fase,
 author = {Huisman, Marieke and Jacobs, Bart},
 title = {Java Program Verification via a {Hoare} Logic with Abrupt Termination},
 booktitle = {FASE'00:},
 year = {2000},
 xxxisbn = {3-540-67261-3},
 pages = {284-303},
 publisher = {Springer},
 xxxaddress = {London, UK},
 }

@INPROCEEDINGS{simulatingreachability,
    author = {T. Lev-Ami and N. Immerman and T. Reps and M. Sagiv and S. Srivastava},
    title = {Simulating Reachability using First-Order Logic},
    booktitle = {CADE'05},
    year = {2005},
    pages = {99-115}
}

@INPROCEEDINGS{sasse-meseguer-wrla06,
	AUTHOR = {R. Sasse and J. Meseguer},
	TITLE = {{Java+ITP}: A Verification Tool Based on {Hoare} Logic and
                     Algebraic Semantics},
xxxeditor = {Grit Denker and Carolyn Talcott},
booktitle = {WRLA'06)},
xxxpublisher = "Elsevier",
series = "ENTCS",
volume = {176},
xxxnumber = {4},
year = {2007},
pages= {29-46},
}

@book{schmidt86,
title = "Denotational Semantics\mdash A Methodology for Language Development",
author = "David A. Schmidt",
year = "1986",
publisher = "Allyn and Bacon, Boston, MA"
}

@Book{Slonneger-Kurtz-1995,
author = {Kenneth Slonneger and Barry L. Kurtz},
title = "Formal Syntax and Semantics of Programming Languages",
publisher = {Addison-Wesley},
year = {1995},
}

@book{Stark2001,
  author    = {Robert F. St{\"a}rk and
               Joachim Schmid and
               Egon B{\"o}rger},
  title     = {Java and the Java Virtual Machine: Definition, Verification,
               Validation},
  publisher = {Springer},
  year      = {2001},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@INPROCEEDINGS{stehr-cinni,
  author    = {Mark-Oliver Stehr},
  title     = {{CINNI} - A Generic Calculus of Explicit Substitutions and
               its Application to lambda-, sigma- and pi- Calculi},
  volume    = {36},
  year      = {2000},
  ee        = {http://www.elsevier.com/gej-ng/31/29/23/71/22/show/Products/notes/index.htt\#006},
  bibsource = {DBLP, http://dblp.uni-trier.de},
	BOOKTITLE = {Proceedings of the Third International Workshop on
                Rewriting Logic and its Applications (WRLA 2000)},
        EDITOR = {K. Futatsugi},
	series = {Electronic Notes in Theoretical Computer Science},
        xxxpublisher = {Elsevier}
}

@UNPUBLISHED{msr-tool,
  title = {An Execution Environment for the {MSR} Cryptoprotocol
                                      Specification Language},
  author = {Mark-Oliver Stehr and Iliano Cervesato and Stefan Reich},
  year = {2004},
  note =   {\verb|http://formal.cs.uiuc.edu/stehr/msr.html|}
}

@INPROCEEDINGS{stehr-talcott-wrla02,
  author    = {Mark-Oliver Stehr and
               Carolyn L. Talcott},
  series   = {Electronic Notes in Theoretical Computer Science},
  volume    = {71},
  pages = {240-260},
  year      = {2002},
  ee        = {http://www1.elsevier.com/gej-ng/31/29/23/145/23/show/Products/notes/index.htt\#014},
  bibsource = {DBLP, http://dblp.uni-trier.de},
	TITLE = {Plan in {Maude}: Specifying an active network programming
                  language},
	BOOKTITLE = {Proceedings of the Forth International Workshop on
                Rewriting Logic and its Applications (WRLA 2002)},
        EDITOR = {F. Gadducci and U. Montanari},
        xxxpublisher = {Elsevier}
}

@InProceedings{StTa05,
  author = 	 {M.-O. Stehr and C.~L.~Talcott},
  title = 	 {Practical Techniques for Language Design and Prototyping},
  booktitle = 	 {Abstracts Collection of the Dagstuhl Seminar 05081 on
                  Foundations of Global Computing. February 20-25, 2005.
                  Schloss Dagstuhl, Wadern, Germany},
  year = 	 {2005},
  editor = 	 {J. L. Fiadeiro and U. Montanari and M. Wirsing}
}

@INPROCEEDINGS{pi-wrla02,
  author    = {Prasanna Thati and
               Koushik Sen and
               Narciso Mart\'{\i}-Oliet},
  title     = {An Executable Specification of Asynchronous {Pi-Calculus}
               Semantics and May Testing in {Maude 2.0.}},
  series   = {Electronic Notes in Theoretical Computer Science},
  volume    = {71},
  year      = {2002},
  ee        = {http://www1.elsevier.com/gej-ng/31/29/23/145/23/show/Products/notes/index.htt\#015},
  bibsource = {DBLP, http://dblp.uni-trier.de},
	BOOKTITLE = {Proceedings of the Forth International Workshop on
                Rewriting Logic and its Applications (WRLA 2002)},
        EDITOR = {F. Gadducci and U. Montanari},
        xxxpublisher = {Elsevier}
}

@article{asf-sdf,
  author    = {Mark van den Brand and
               Jan Heering and
               Paul Klint and
               Pieter A. Olivier},
  title     = {Compiling language definitions: the ASF+SDF compiler},
  journal   = {ACM Transactions on Programming Languages and Systems (TOPLAS)},
  volume    = {24},
  number    = {4},
  year      = {2002},
  pages     = {334-368},
  ee        = {http://doi.acm.org/10.1145/567097.567099},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@BOOK{asf-book,
	AUTHOR = {A. van Deursen and J. Heering and P. Klint},
	TITLE = {Language Prototyping: An Algebraic Specification
                  Approach},
	publisher = {World Scientific},
	YEAR = {1996}
}

@PHDTHESIS{verdejo-thesis,
	AUTHOR = {A. Verdejo},
	TITLE = {Maude como marco sem\'antico ejecutable},
	SCHOOL = {Facultad de Inform\'{a}tica,
                  Universidad Complutense, Madrid, Spain},
	YEAR = {2003}
}

@INPROCEEDINGS{ccs-wrla02,
	AUTHOR = {Alberto Verdejo and Narciso Mart\'{\i}-Oliet},
	TITLE = {Implementing {CCS} in {Maude 2}},
	BOOKTITLE = {Proceedings of the Forth International Workshop on
                Rewriting Logic and its Applications (WRLA 2002)},
        EDITOR = {F. Gadducci and U. Montanari},
        xxxpublisher = {Elsevier},
  series   = {Electronic Notes in Theoretical Computer Science},
  volume    = {71},
  year      = {2002},
  ee        = {http://www1.elsevier.com/gej-ng/31/29/23/145/23/show/Products/notes/index.htt\#016},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}}

@article{maude-sos,
  author    = {Alberto Verdejo and
               Narciso Mart\'{\i}-Oliet},
  title     = {Executable structural operational semantics in {Maude}},
  journal   = {Journal of Logic \& Algebraic Programming},
  volume    = {67},
  number    = {1-2},
  year      = {2006},
  pages     = {226-293},
  ee        = {http://dx.doi.org/10.1016/j.jlap.2005.09.008},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{viry-tcs,
  author    = {Patrick Viry},
  title     = {Equational rules for rewriting logic},
  journal   = {Theoretical Computer Science},
  volume    = {285},
  number    = {2},
  year      = {2002},
  pages     = {487-517},
  ee        = {http://dx.doi.org/10.1016/S0304-3975(01)00366-8},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{stratego,
  author    = {Eelco Visser},
  title     = {Program Transformation with {Stratego/XT}: Rules, Strategies,
               Tools, and Systems in {Stratego/XT} 0.9.},
  year      = {2003},
  pages     = {216-238},
  ee        = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3016{\&}spage=216},
  editor    = {Christian Lengauer and
               Don S. Batory and
               Charles Consel and
               Martin Odersky},
  booktitle     = {Domain-Specific Program Generation, International Seminar,
               Dagstuhl Castle, Germany, March 23-28, 2003, Revised Papers},
  xxxpublisher = {Springer},
  series    = {LNCS},
  volume    = {3016},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

#@proceedings{DBLP:conf/dagstuhl/2003dspg,
  editor    = {Christian Lengauer and
               Don S. Batory and
               Charles Consel and
               Martin Odersky},
  title     = {Domain-Specific Program Generation, International Seminar,
               Dagstuhl Castle, Germany, March 23-28, 2003, Revised Papers},
  booktitle = {Domain-Specific Program Generation},
  xxxpublisher = {Springer},
  series    = {LNCS},
  volume    = {3016},
  year      = {2004},
  isbn      = {3-540-22119-0},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{wadler92,
 author = {Philip Wadler},
 title = {The essence of functional programming},
 booktitle = {POPL'92: Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
 year = {1992},
 isbn = {0-89791-453-8},
 pages = {1-14},
 location = {Albuquerque, New Mexico, United States},
 doi = {http://doi.acm.org/10.1145/143165.143169},
 xxxpublisher = {ACM Press},
 address = {New York, NY, USA},
 }

@article{wand80-fsh,
  author    = {Mitchell Wand},
  title     = {First-Order Identities as a Defining Language},
  journal   = {Acta Informatica},
  volume    = {14},
  year      = {1980},
  pages     = {337-357},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{reduction-semantics,
  author    = {A.K. Wright and
               M. Felleisen},
  title     = {A Syntactic Approach to Type Soundness},
  journal   = {Inf.~\& Computation},
  volume    = {115},
  number    = {1},
  year      = {1994},
  pages     = {38-94},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{felleisen-hieb-92,
  author    = {Matthias Felleisen and
               Robert Hieb},
  title     = {The Revised Report on the Syntactic Theories of Sequential
               Control and State},
  journal   = {Th. Comp. Sci.},
  volume    = {103},
  number    = {2},
  year      = {1992},
  pages     = {235-271},
  ee        = {http://dx.doi.org/10.1016/0304-3975(92)90014-7},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@INPROCEEDINGS{Barnett04thespec,
    author = {Mike Barnett and K. Rustan M. Leino and Wolfram Schulte},
    title = {The {Spec}\# Programming System},
    year = {2004},
    booktitle = {CASSIS'04},
    volume = {3362},
    pages = {49-69},
    series = {LNCS},
    xxxpublisher = {Springer}
}

@inproceedings{conf/fmco/BerdineCO05,
  author = {Josh Berdine and Cristiano Calcagno and Peter W. O'Hearn},
  booktitle = {FMCO'06},
  xxxeditor = {Frank S. de Boer and Marcello M. Bonsangue and Susanne Graf and Willem P. de Roever},
  interHash = {751f75880da11f83233082b5fb4182b9},
  intraHash = {9f97ae9be53964df82386fec58b4389c},
  pages = {115-137},
  xxxpublisher = {Springer},
  series = {LNCS},
  title = {Smallfoot: Modular Automatic Assertion Checking with Separation Logic.},
  volume = {4111},
  year = {2006},
  ee = {http://dx.doi.org/10.1007/11804192_6},
  date = {2006-12-15}
}

@article{DBLP:journals/acta/Gries79,
  author    = {David Gries},
  title     = {The {Schorr-Waite} Graph Marking Algorithm},
  journal   = {Acta Informatica},
  volume    = {11},
  year      = {1979},
  pages     = {223-232},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{hubert-marche-schorr-waite,
  author    = {Thierry Hubert and
               Claude March{\'e}},
  title     = {A case study of {C} source code verification: the {Schorr-Waite}
               algorithm},
  booktitle = {SEFM},
  year      = {2005},
  pages     = {190-199},
  ee        = {http://doi.ieeecomputersociety.org/10.1109/SEFM.2005.1},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{FilliatreM04,
  author    = {Jean-Christophe Filli{\^a}tre and Claude March{\'e}},
  title     = {Multi-prover Verification of {C} Programs},
  booktitle = {ICFEM'04},
  year      = {2004},
  pages     = {15-29},
  series	= {LNCS},
  volume    = {3308},
  ee        = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3308{\&}spage=15},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

	
@article{1236121,
 author = {O'Hearn, Peter W.},
 title = {Resources, concurrency, and local reasoning},
 journal = {Theoretical Computer Science},
 volume = {375},
 number = {1-3},
 year = {2007},
 pages = {271-307},
 xxxpublisher = {Elsevier Science xxxpublishers Ltd.},
 address = {Essex, UK},
 }

@INPROCEEDINGS{Berdine05symbolicexecution,
    author = {Josh Berdine and Cristiano Calcagno and Peter W. O'Hearn},
    title = {Symbolic Execution with Separation Logic},
    booktitle = {APLAS'05},
    year = {2005},
    series = {LNCS},
    volume = {3780},
    pages = {52-68},
    xxxpublisher = {Springer}
}

@inproceedings{1111048,
  author    = {Shuvendu K. Lahiri and
               Shaz Qadeer},
  title     = {Verifying properties of well-founded linked lists},
  booktitle = {POPL},
  year      = {2006},
  pages     = {115-126},
  ee        = {http://doi.acm.org/10.1145/1111037.1111048},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@TechReport{havocChecking,
	author = {Brian Hackett and Shuvendu Lahiri and Shaz Qadeer and Thomas Ball},
	title  ={Scalable Modular Checking of System-Specific Properties: Myth or Reality?},
	year = {2008},
	institution = {Microsoft Research},
	number = {MSR-TR-2008-82}
}

@inproceedings{Logic-verification-spin,
	abstract = {We describe a tool, called AX, that can be used in combination with
the model checker SPIN to efficiently verify logical properties of distributed
software systems implemented in ANSI-standard C [18]. AX, short for
Automaton eXtractor, can extract verification models from C code at a user
defined level of abstraction. Target applications include telephone switching
software, distributed operating systems code, protocol implementations, concurrency
control methods, and client-server...},
	author = {Holzmann, Gerard J.},
	booktitle = {Proc. of the 7th International {SPIN} {W}orkshop},
	citeulike-article-id = {1339594},
	citeulike-linkout-0 = {http://citeseer.ist.psu.edu/holzmann00logic.html},
	citeulike-linkout-1 = {http://citeseer.lcs.mit.edu/holzmann00logic.html},
	citeulike-linkout-2 = {http://citeseer.ifi.unizh.ch/holzmann00logic.html},
	citeulike-linkout-3 = {http://citeseer.comp.nus.edu.sg/holzmann00logic.html},
	keywords = {checking, model},
	posted-at = {2007-05-28 23:44:59},
	priority = {3},
	xxxpublisher = {Springer},
	title = {Logic Verification of ANSI-{C} code with {SPIN}},
	url = {http://citeseer.ist.psu.edu/holzmann00logic.html},
	volume = {1885},
	year = {2000}
}

@inproceedings{DBLP:conf/tacas/MouraB08,
  author    = {Leonardo Mendon\c{c}a de Moura and
               Nikolaj Bj{\o}rner},
  title     = {Z3: An Efficient {SMT} Solver},
  booktitle = {TACAS},
  year      = {2008},
  pages     = {337-340},
  volume    = {4963},
  series    = {LNCS},
  xxxisbn      = {978-3-540-78799-0},
  ee        = {http://dx.doi.org/10.1007/978-3-540-78800-3_24},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/cav/BarrettT07,
  author    = {Clark Barrett and
               Cesare Tinelli},
  title     = {{CVC3}},
  bookTitle = "CAV'07",
  year      = {2007},
  pages     = {298-302},
  ee        = {http://dx.doi.org/10.1007/978-3-540-73368-3_34},
  series    = {LNCS},
  volume    = {4590},
}

@inproceedings{yices,
  author    = {Bruno Dutertre},
  title     = {Yices 2.2},
  booktitle = {CAV'14},
  pages     = {737-744},
  series    = {LNCS},
  volume    = {8559},
  year      = {2014},
}

@inproceedings{DBLP:conf/cav/BarrettCDHJKRT11,
  author    = {Clark Barrett and
               Christopher L. Conway and
               Morgan Deters and
               Liana Hadarean and
               Dejan Jovanovic and
               Tim King and
               Andrew Reynolds and
               Cesare Tinelli},
  title     = {{CVC4}},
  booktitle = {CAV'11},
  series    = {LNCS},
  volume    = {6806},
  publisher = {Springer},
  pages     = {171-177},
  year      = {2011},
  url       = {http://dx.doi.org/10.1007/978-3-642-22110-1_14},
  doi       = {10.1007/978-3-642-22110-1_14},
  timestamp = {Sat, 17 May 2014 20:54:48 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/cav/BarrettCDHJKRT11},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@TechReport{verificationConditionSplitting,
	author = {K. Rustan M. Leino and Michal Moskal and Wolfram Schulte},
	title  ={Verification Condition Splitting},
	year = {2008},
	number= {KRML 192},
	institution = {Microsoft Research}
}

@TechReport{vcc,
	author = {Ernie Cohen and Michal Moskal and Wolfram Schulte and Stephan Tobies},
	title  = {A Practical Verification Methodology for Concurrent Programs},
	year = {2009},
	institution = {Microsoft Research},
	number = {MSR-TR-2009-15}
}

@inproceedings{1449782,
 author = {Distefano, Dino and Parkinson, Matthew J.},
 title = {{jStar}: Towards practical verification for {Java}},
 booktitle = {OOPSLA'08},
 year = {2008},
 pages = {213-226},
 location = {Nashville, TN, USA},
 publisher = {ACM},
 }

@INPROCEEDINGS{Cok04esc/java2:uniting,
    author = {David R. Cok and Joseph R. Kiniry},
    title = {{ESC/Java2}: Uniting \mbox{{ESC}/{Java}} and {JML}: Progress and issues in building and using {ESC/Java2}},
    booktitle = {CASSIS'04},
    volume = {3362},
    pages = {108-128},
    series = {LNCS},
    year = {2004},

    xxxpublisher = {Springer}
}

@inproceedings{512558,
  author    = {Cormac Flanagan and
               K. Rustan M. Leino and
               Mark Lillibridge and
               Greg Nelson and
               James B. Saxe and
               Raymie Stata},
  title     = {Extended Static Checking for {Java}},
  booktitle = {PLDI},
  year      = {2002},
  pages     = {234-245},
  ee        = {http://doi.acm.org/10.1145/512529.512558},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{citeulike:2868751,
  author    = {Jean-Christophe Filli{\^a}tre and
               Claude March{\'e}},
  title     = {The {Why}/{Krakatoa}/{Caduceus} Platform for Deductive Program
               Verification},
  booktitle = {CAV},
  year      = {2007},
  pages     = {173-177},
  ee        = {http://dx.doi.org/10.1007/978-3-540-73368-3_21},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{Distefano06alocal,
  author    = {Dino Distefano and
               Peter W. O'Hearn and
               Hongseok Yang},
  title     = {A Local Shape Analysis Based on Separation Logic},
  booktitle = {TACAS},
  year      = {2006},
  pages     = {287-302},
  series    = {LNCS},
  volume    = {3920},
  ee        = {http://dx.doi.org/10.1007/11691372_19},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@techreport{citeulike:3721776,
	abstract = {This note describes a separation-logic-based approach for the specification
and verification of safety properties of pointer-manipulating
imperative programs.We describe the approach for the C language.
The safety properties to be verified are specified as annotations
in the source code, in the form of function preconditions and postconditions
expressed as separation logic assertions. To enable rich
specifications, the user may include additional annotations that define
inductive datatypes, primitive recursive pure functions over
these datatypes, and abstract predicates (i.e. named, parameterized
assertions). A restricted form of existential quantification is supported
in assertions in the form of pattern matching.
Verification is based on forward symbolic execution, where
memory is represented as a separate conjunction of points-to assertions
and abstract predicate assertions, and data values are represented
as first-order logic terms with a set of constraints. Abstract
predicates must be folded and unfolded explicitly using ghost
statements. Rewritings of the abstract state that require induction,
or derivations of facts over data values that require induction, can
be done by defining lemma functions, which are like ordinary C
functions except that it is checked that they terminate. Specifically,
when a lemma function performs a recursive call, either the recursive
call must apply to a strict subset of memory, or one of its parameters
must be an inductive value whose size decreases at each
recursive call.
Assertions over data values are delegated to an SMT solver,
formulated as queries against an axiomatization of the inductive
datatypes and recursive pure functions. Importantly, no exhaustiveness
axioms are included in this axiomatization; this prevents the
SMT solver from performing case analysis on inductive values.
Combined with a measure to prevent infinite reductions due to selffeeding
recursions, this ensures termination of the SMT solver.
The time complexity of verification is unbounded in theory.
Specifically, since recursive pure functions of arbitrary time complexity
may be defined, there is no bound on the time complexity
of SMT queries. Furthermore, the approach, as currently implemented,
does not perform joining of symbolic execution paths after
conditional constructs; therefore, the number of symbolic execution
steps is exponential in the number of such constructs. However,
since no significant search is performed implicitly by the verifier or
the SMT solver, performance is very good in practice.
A prototype implementation and example annotated programs
are available at http://www.cs.kuleuven.be/\~{}bartj/verifast/.},
	author = {Jacobs, Bart and Piessens, Frank},
	citeulike-article-id = {3721776},
	citeulike-linkout-0 = {http://www.cs.kuleuven.be/~bartj/verifast/verifast.pdf},
	institution = {K.U.~Leuven},
	keywords = {c, static-verification, verifast},
	xxxmonth = {August},
	posted-at = {2008-11-28 14:05:13},
	priority = {0},
	title = {The {VeriFast} Program Verifier},
	number = {CW-520},
	year = {2008}
}
@inproceedings{smallfootrg,
 author = {Cristiano Calcagno and Matthew J. Parkinson and Viktor Vafeiadis},
 title = {Modular safety checking for fine-grained concurrency},
 booktitle = {SAS'07},
 volume = {4634},
 year = {2007},
 pages = {233-248},
 xxxpublisher = {Springer},
 }

@inproceedings{DBLP:conf/tphol/Tuerk09,
  author    = {Thomas Tuerk},
  title     = {A Formalisation of Smallfoot in HOL},
  booktitle = {TPHOLs},
  year      = {2009},
  pages     = {469-484},
  ee        = {http://dx.doi.org/10.1007/978-3-642-03359-9_32},
  crossref  = {DBLP:conf/tphol/2009},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/tphol/2009,
  editor    = {Stefan Berghofer and
               Tobias Nipkow and
               Christian Urban and
               Makarius Wenzel},
  title     = {Theorem Proving in Higher Order Logics, 22nd International
               Conference, TPHOLs 2009, Munich, Germany, August 17-20,
               2009. Proceedings},
  booktitle = {TPHOLs},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {5674},
  year      = {2009},
  isbn      = {978-3-642-03358-2},
  ee        = {http://dx.doi.org/10.1007/978-3-642-03359-9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

 @MISC{RanTin-SMTLIB,
  author =	 {Clark Barrett and Silvio Ranise and Aaron Stump and Cesare Tinelli},
  title =	 {{The Satisfiability Modulo Theories Library}},
  url = {http://www.smt-lib.org/},
  year =	 2008,
}

@article{363554,
 author = {Schorr, H. and Waite, W. M.},
 title = {An efficient machine-independent procedure for garbage collection in various list structures},
 journal = {Commun. ACM},
 volume = {10},
 number = {8},
 year = {1967},
 pages = {501-506},
 xxxpublisher = {ACM},
 address = {New York, NY, USA},
 }

@misc{kmaude,
	author = {Traian Florin {\c S}erb{\u a}nu{\c t}{\u a}},
	title  ={K-Maude Website},
	year = {2009},
	url = {http://fsl.cs.uiuc.edu/index.php/K-Maude}
}

@Article{smtcomp08,
	author = {Clark Barrett and Morgan Deters and Albert Oliveras and Aaron Stump},
	title = {Design and results of the 4th annual satisfiability modulo theories competition},
	year  = {2008},
	journal = {In Preparation}
}

@INPROCEEDINGS{Barnett06boogie:a,
    author = {Mike Barnett and Bor-yuh Evan Chang and Robert DeLine
and Bart Jacobs and K. Rustan M. Leino},
    title = {Boogie: A modular reusable verifier for object-oriented programs},
    booktitle = {FMCO'05},
    volume={4111},
    series={LNCS},
    year = {2006},
    pages = {364-387},
}

@INPROCEEDINGS{Alexey06automatedverification,
    author = {Alexey Loginov and Thomas Reps and Mooly Sagiv},
    title = {Automated Verification of the {D}eutsch-{S}chorr-{W}aite Tree-Traversal Algorithm},
    booktitle = {SAS'06},
    series={LNCS},
    volume={4134},
    pages={261-279},
    year = {2006},
    xxxpublisher = {Springer}
}
 @article{burdy03overview,
   author = {Lilian Burdy and Yoonsik Cheon and David Cok and Michael D.
	Ernst and Joe Kiniry and Gary T. Leavens and K. Rustan M. Leino
	and Erik Poll},
   title = {An overview of {JML} tools and applications},
   journal = {Software Tools for Technology Transfer},
   volume = {7},
   number = {3},
   pages = {212-232},
   xxxmonth = jun,
   year = {2005}
}


@article{Sagiv99parametricshape,
  author    = {Shmuel Sagiv and
               Thomas W. Reps and
               Reinhard Wilhelm},
  title     = {Parametric shape analysis via 3-valued logic},
  journal   = {ACM Trans. Prog. Lang. Syst.},
  volume    = {24},
  number    = {3},
  year      = {2002},
  pages     = {217-298},
  ee        = {http://doi.acm.org/10.1145/514188.514190},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

  author    = {G.D. Plotkin},
  title     = {A structural approach to operational semantics},
  journal   = {Journal of Logic \& Algebraic Programming},
  volume    = {60-61},
  year      = {2004},
  pages     = {17-139},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  xxxnote = {Original version: University of Aarhus Technical Report DAIMI FN-19, 1981}

--cut--

@article{1236122,
 author = {Yang, Hongseok},
 title = {Relational Separation Logic},
 journal = {Theoretical Computer Science},
 volume = {375},
 number = {1-3},
 year = {2007},
 xxxissn = {0304-3975},
 pages = {308-334},
 xxxdoi = {http://dx.doi.org/10.1016/j.tcs.2006.12.036},
 xxxpublisher = {Elsevier},
 xxxaddress = {Essex, UK},
 }

@article{OHearn99thelogic,
  author    = {Peter W. O'Hearn and
               David J. Pym},
  title     = {The logic of bunched implications},
  journal   = {Bulletin of Symbolic Logic},
  volume    = {5},
  number    = {2},
  year      = {1999},
  pages     = {215-244},
  ee        = {http://www.math.ucla.edu/$\sim$asl/bsl/0502/0502-003.ps},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@INPROCEEDINGS{Yang01anexample,
    author = {Hongseok Yang},
    title = {An example of local reasoning in {BI} pointer logic: The {Schorr-Waite} graph marking algorithm},
    booktitle = {SPACE'01},
    year = {2001}
}


@Book{KeYBook2007,
   editor =        {Bernhard Beckert and Reiner H\"ahnle and Peter H. Schmitt},
   title =         {Verification of Object-Oriented Software: The
{KeY} Approach},
   volume =    {4334},
   series        = {LNCS},
   publisher     = {Springer},
   year          = {2007}
}

@MISC{Leavens99jml:a,
    author = {Gary T. Leavens and Albert L. Baker and Clyde Ruby},
    title = {JML: A Notation for Detailed Design},
    year = {1999}
}

@inproceedings{WBO08,
  author    = {Shuling Wang and
               L. S. Barbosa and
               J. N. Oliveira},
  title     = {A Relational Model for Confined Separation Logic},
  booktitle = {TASE'08},
  xxxpublisher = {IEEE},
  year      = {2008},
  pages     = {263-270},
  ee        = {http://doi.ieeecomputersociety.org/10.1109/TASE.2008.38}
}

@article{1498929,
 author = {O'Hearn, Peter W. and Yang, Hongseok and Reynolds, John C.},
 title = {Separation and information hiding},
 journal = {ACM Transactions on Programming Languages and Systems},
 volume = {31},
 number = {3},
 year = {2009},
 xxxissn = {0164-0925},
 pages = {1-50},
 xxxdoi = {http://doi.acm.org/10.1145/1498926.1498929},
 xxxpublisher = {ACM},
 xxxaddress = {New York, NY, USA},
 }

@article{PALE,
 author = {M{\o}ller, Anders and Schwartzbach, Michael I.},
 title = {The pointer assertion logic engine},
 journal = {SIGPLAN Not.},
 volume = {36},
 number = {5},
 year = {2001},
 xxxissn = {0362-1340},
 pages = {221-231},
 xxxdoi = {http://doi.acm.org/10.1145/381694.378851},
 xxxpublisher = {ACM},
 xxxaddress = {New York, NY, USA},
 }


@inproceedings{DBLP:conf/cav/McPeakN05,
  author    = {Scott McPeak and
               George C. Necula},
  title     = {Data Structure Specifications via Local Equality Axioms},
  booktitle = {CAV'05},
  xxxpublisher = {Springer},
  series    = {LNCS},
  volume    = {3576},
  year      = {2005},
  pages     = {476-490},
  ee        = {http://dx.doi.org/10.1007/11513988_47},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@inproceedings{DBLP:conf/popl/RinetzkyBRSW05,
  author    = {Noam Rinetzky and
               J{\"o}rg Bauer and
               Thomas W. Reps and
               Shmuel Sagiv and
               Reinhard Wilhelm},
  title     = {A semantics for procedure local heaps and its abstractions},
  booktitle = {POPL'05},
  year      = {2005},
  pages     = {296-309},
  ee        = {http://doi.acm.org/10.1145/1040305.1040330},
  xxxpublisher = {ACM},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  idea      = {The give a different semantics for a language and use
that to develope an abstract interpretation and prove something like
destructive merge of two lists.}
}

@article{DBLP:journals/toplas/BieringBT07,
  author    = {Bodil Biering and
               Lars Birkedal and
               Noah Torp-Smith},
  title     = {BI-hyperdoctrines, higher-order separation logic, and
abstraction},
  journal   = {TOPLAS},
  volume    = {29},
  number    = {5},
  year      = {2007},
  ee        = {http://doi.acm.org/10.1145/1275497.1275499},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/esop/BieringBT05,
  author    = {Bodil Biering and
               Lars Birkedal and
               Noah Torp-Smith},
  title     = {BI Hyperdoctrines and Higher-Order Separation Logic},
  series    = {LNCS},
  xxxpublisher = {Springer},
  booktitle = {ESOP},
  volume    = {3444},
  year      = {2005},
  pages     = {233-247},
  ee        = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3444{\&}spage=233},
  ocrossref  = {DBLP:conf/esop/2005},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  idea      = {The propose a logic in which separation logic and all
their extensions are definable.}
}

@article{DBLP:journals/iandc/MehtaN05,
  author    = {Farhad Mehta and
               Tobias Nipkow},
  title     = {Proving pointer programs in higher-order logic},
  journal   = {Inf.~\& Computation},
  volume    = {199},
  number    = {1-2},
  year      = {2005},
  pages     = {200-227},
  ee        = {http://dx.doi.org/10.1016/j.ic.2004.10.007},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  idea      = {Uses a semantic of heap as mapping from name to values,
then proves Schorre-Waitte in Isabelle.}
}

@article{DBLP:journals/fac/Nipkow98,
  author    = {Tobias Nipkow},
  title     = {Winskel is (almost) Right: Towards a Mechanized Semantics},
  journal   = {Formal Aspects of Computing},
  volume    = {10},
  number    = {2},
  year      = {1998},
  pages     = {171-186},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@INPROCEEDINGS{Harel84dynamiclogic,
    author = {David Harel and Dexter Kozen and Jerzy Tiuryn},
    title = {Dynamic Logic},
    booktitle = {Handbook of Philosophical Logic},
    year = {1984},
    pages = {497-604},
    xxxpublisher = {MIT}
}

@INPROCEEDINGS{Magill-inferring,
    author = {Magill, S. and  Nanevski, A. and Clarke, E. and Lee, P.},
    title = {Inferring invariants in Separation Logic for imperative
list-processing programs},
    booktitle = {SPACE'06},
    year = {2006}
}
@inproceedings{alias-logic,
 author = {Bozga, Marius and Iosif, Radu and Laknech, Yassine},
 title = {Storeless semantics and alias logic},
 booktitle = {PEPM'03},
 year = {2003},
 xxxisbn = {1-58113-667-6},
 pages = {55-65},
 xxxlocation = {San Diego, California, USA},
 xxxdoi = {http://doi.acm.org/10.1145/777388.777395},
 xxxpublisher = {ACM},
 xxxaddress = {New York, NY, USA},
}

@inproceedings{Floyd:AssignMeaningProg,
  key =          "Floyd",
  author =       "R. W. Floyd",
  title =        "Assigning Meaning to Programs",
  booktitle =    "Symposium on Applied Mathematics",
  volume =       "19",
  year =         "1967",
  pages =        "19-32",
}

@INCOLLECTION{gordon-collavizza,
	author={M.J.C. Gordon and H. Collavizza},
	title={Forward with {Hoare}},
	booktitle={Reflections on the Work of {C.A.R.~Hoare}},
	xxxeditor={Roscoe, A.W. and Jones, C.B. and Wood, K.},
	series={History of Computing Series},
	publisher={Springer},
	year={2010}
}

@techreport{c99,
	author = {{ISO/IEC  JTC 1, SC 22, WG 14}},
	Institution = {International Organization for Standardization},
	Title = {{ISO/IEC} 9899:1999: Programming Languages--{C}},
	Month={December},
	Year = {1999}
}

@article{meseguer-1992-tcs,
 author = {Meseguer, Jos\'{e}},
 title = {Conditional rewriting logic as a unified model of concurrency},
 journal = TCS,
 volume = {96},
 number = {1},
 year = {1992},
 xxxissn = {0304-3975},
 pages = {73-155},
 xxxdoi = {http://dx.doi.org/10.1016/0304-3975(92)90182-F},
 publisher = {Elsevier},
 xxxaddress = {Essex, UK},
 }

@inproceedings{serbanuta-rosu-2010-wrla,
  title={ {K-Maude}:  A Rewriting Based Tool for Semantics of Programming Languages},
  author={Traian Florin {\c S}erb{\u a}nu{\c t}{\u a} and Grigore Ro{\c s}u},
  booktitle={8th International Workshop on Rewriting Logic and its Applications (WRLA'09)},
  series={LNCS},
  volume={6381},
  year={2010},
  pages={104-122},
  xxxnote={To appear},
}

@TechReport{meredith-hills-rosu-2007-tr-b,
author = {Patrick Meredith and Mark Hills and Grigore Ro\c{s}u},
title = "A {K} Definition of {Scheme}",
institution = {University of Illinois at Urbana-Champaign},
Number     = {Department of Computer Science UIUCDCS-R-2007-2907},
Year       = {2007}
}

@techreport{c1x,
	Author = {{ISO/IEC  JTC 1, SC 22, WG 14}},
	Institution = {International Organization for Standardization},
	Title = {{ISO/IEC} 9899:201x: Programming Languages--{C}},
	Type = {Committee Draft},
	Month = {August},
	Year = {2011}
}

@inproceedings{meseguer-rosu-2011-fct,
  author    = {Jos\'e Meseguer and Grigore Ro\c{s}u},
  title     = {The Rewriting Logic Semantics Project: A Progress Report},
  booktitle = {Proceedings of the 17th International Symposium on Fundamentals of Computation Theory (FCT'11)},
  year      = {2011},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {to appear, 2011},
  note      = {Invited talk},
}

@InProceedings{tang-osdi2010,
  author = 	 {Shuo Tang, Haohui Mai and Samuel T. King},
  title = 	 {Trust and Protection in the Illinois Browser
Operating System},
  note = 	 {to appear in Proceedings of the Symposium on Operating Systems Design and Implementation (OSDI), October 2010},
}


@inproceedings{DBLP:conf/sp/ChenMeseguerSasseWangWangSWW07,
  author    = {Shuo Chen and
               Jos{\'e} Meseguer and
               Ralf Sasse and
               Helen J. Wang and
               Yi-Min Wang},
  title     = {A Systematic Approach to Uncover Security Flaws in GUI Logic},
  booktitle = {IEEE Symposium on Security and Privacy},
  year      = {2007},
  pages     = {71-85},
  ee        = {http://dx.doi.org/10.1109/SP.2007.6},
  crossref  = {DBLP:conf/sp/2007},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/sp/2007,
  title     = {2007 IEEE Symposium on Security and Privacy (S{\&}P 2007),
               20-23 May 2007, Oakland, California, USA},
  booktitle = {IEEE Symposium on Security and Privacy},
  publisher = {IEEE Computer Society},
  year      = {2007},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{rosu-stefanescu-2012-oopsla,
  author    = {Grigore Rosu and Andrei Stefanescu},
  title     = {Checking Reachability using Matching Logic},
  booktitle = {OOPSLA'12},
  pages     = {555-574},
  year      = {2012},
  publisher = {ACM},
  ee        = {http://doi.acm.org/10.1145/2384616.2384656},
}

@INPROCEEDINGS{Berdine05smallfoot:modular,
    author = {Josh Berdine and Cristiano Calcagno and Peter W. O’hearn},
    title = {Smallfoot: Modular automatic assertion checking with separation logic},
    booktitle = {Formal Methods for Components and Objects (FMCO'05)},
    year = {2005},
    pages = {115-137},
    publisher = {Springer}
}


@article{rosu-serbanuta-2010-jlap,
  title={An Overview of the {K} Semantic Framework},
  author={Grigore Ro{\c s}u and Traian Florin {\c S}erb{\u a}nu{\c t}{\u a} },
  journal={Journal of Logic and Algebraic Programming},
  volume={79},
  number={6},
  pages={397-434},
  year={2010},
}

@article{meredith-jin-chen-rosu-2009-jase,
  author={Patrick Meredith and Dongyun Jin and Feng Chen and Grigore Ro\c{s}u},
  title={Efficient Monitoring of Parametric Context-Free Patterns},
  journal={J. Automated Software Engineering},
  volume={17},
  number={2},
  publisher={Springer Netherlands},
  month={June},
  year={2010},
  pages={149-180}
}

@inproceedings{bodden-chen-rosu-2009-aosd,
title={Dependent advice: A general approach to optimizing history-based Aspects},
author={Eric Bodden and Feng Chen and Grigore Ro\c{s}u},
booktitle={Aspect-Oriented Software Development (AOSD'09)},
year={2009},
 pages = {3-14},
 publisher = {ACM}
}

@techreport{rosu-ellison-schulte-2009-tr,
author={Grigore Ro\c{s}u and Chucky Ellison and Wolfram Schulte},
title={From Rewriting Logic Executable Semantics to Matching Logic Program Verification},
number={http://hdl.handle.net/2142/13159},
institution={University of Illinois},
year={2009},
xxxmonth={July},
url={http://hdl.handle.net/2142/13159}
}

@inproceedings{rosu-schulte-serbanuta-2009-rv,
  author={G. Ro\c{s}u and W. Schulte and T.F. \c{S}erb\u{a}nu\c{t}\u{a}},
  title={Runtime Verification of {C} Memory Safety},
  booktitle={RV'09},
  year={2009},
  series = {LNCS},
  note={to appear}
}

@inproceedings{hubert-marche-sefm-05,
 author = {Hubert, Thierry and March\'{e}, Claude},
 title = {A case study of {C} Source Code Verification: The {Schorr-Waite} Algorithm},
 booktitle = {SEFM'05},
 year = {2005},
 pages = {190-199},
 publisher = {IEEE},
 }

@INPROCEEDINGS{Alexey06automatedverification,
    author = {Alexey Loginov and Thomas Reps and Mooly Sagiv},
    title = {Automated Verification of the {D}eutsch-{S}chorr-{W}aite Tree-Traversal Algorithm},
    booktitle = {SAS'06},
    year = {2006},
    xxxpublisher = {Springer}
}



@article{DBLP:journals/acta/Gries79,
  author    = {David Gries},
  title     = {The {Schorr-Waite} Graph Marking Algorithm},
  journal   = {Acta Inf.},
  volume    = {11},
  year      = {1979},
  pages     = {223-232},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}



@techreport{rosu-schulte-2009-tr,
  author={Grigore Ro\c{s}u and W. Schulte},
  title={Matching Logic--Extended Report},
  number={UIUCDCS-R-2009-3026},
  institution={Univ. of Illinois},
  year=2009,
  xxxmonth={January},
}



@inproceedings{javafan-cav,
  author    = {A. Farzan and
               F. Chen and
               J. Meseguer and
               G. Ro\c{s}u},
  title     = {Formal Analysis of {Java} Programs in {JavaFAN}},
  year      = {2004},
  pages     = {501-505},
  booktitle     = {CAV'04},
  xxxpublisher = {Springer},
  series    = {LNCS},
  volume    = {3114}
}


@misc{ML-website,
author={Chucky Ellison and Grigore Ro\c{s}u},
title={Matching logic website\emdash{}{T}ools and examples},
year=2009,
url={http://fsl.cs.uiuc.edu/ml}
}

@misc{llvm,
author={Chris Lattner},
title={LLVM Website},
year=2002,
url={http://llvm.org}
}

@article{meseguer-rosu-2006-tcs,
  author    = {J. Meseguer and
               G. Ro\c{s}u},
  title     = {The rewriting logic semantics project},
  journal   = {Theoretical Computer Science},
  volume    = {373},
  number    = {3},
  year      = {2007},
  pages     = {213-237},
  ee        = {http://dx.doi.org/10.1016/j.tcs.2006.12.018},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}



@inproceedings{soot,
 author               = {Raja Vall\'ee-Rai and Laurie Hendren and Vijay Sundaresan and Patrick Lam and Etienne Gagnon and Phong Co},
 booktitle            = {Proceedings of CASCON 1999},
 pages                = {125-135},
 title                = {Soot - a Java Optimization Framework},
 url                  = {www.sable.mcgill.ca/publications},
 year                 = {1999},
}

@article{FilliatreM04,
	abstract = {Our goal is the verification of C programs at the source code level using formal proof tools. Programs are specified using annotations such as pre- and post-conditions and global invariants. An original approach is presented which allows to formally prove that a function implementation satisfies its specification and is free of null pointer dereferencing and out-of-bounds array access. The method is not bound to a particular back-end theorem prover. A significant part of the ANSI C language is supported, including pointer arithmetic and possible pointer aliasing. We describe a prototype tool and give some experimental results. Keywords: C programming language, Hoare logic, pointer programs, formal verification and proof.},
	author = {Filli\^{a}tre, Jean-Christophe and March\'{e}, Claude},
	citeulike-article-id = {2865757},
	citeulike-linkout-0 = {http://www.springerlink.com/content/ejxv14xdjf5676u5},
	journal = {Formal Methods and Software Engineering},
	keywords = {caduceus, program-analysis},
	pages = {15-29},
	posted-at = {2008-06-05 15:50:48},
	priority = {2},
	title = {Multi-prover Verification of {C} Programs},
	year = {2004}
}

@INPROCEEDINGS{Barnett04thespec,
    author = {Mike Barnett and K. Rustan M. Leino and Wolfram Schulte},
    title = {The {Spec}\# Programming System},
    year = {2004},
    booktitle = {CASSIS'04},
    volume = {3362},
    pages = {49-69},
    series = {LNCS},
    xxxpublisher = {Springer}
}

@inproceedings{dacapo,
 author               = {S. M. Blackburn and et al.},
 booktitle            = {OOPSLA'06},
 title                = {The {DaCapo} Benchmarks: {J}ava Benchmarking Development and Analysis},
 year                 = {2006},
}

@inproceedings{chen-rosu-2007-cav,
author = {Feng Chen and Grigore Ro\c{s}u},
title = "{Parametric and Sliced Causality}",
booktitle = {Computer Aided Verification (CAV'07)},
publisher = {Springer},
series    = {LNCS},
year      = {2007},
volume    = {4590},
pages    =  {240 - 253}
}

@inproceedings{chen-serbanuta-rosu-2008-icse,
  author = {Feng Chen
    and Traian Florin {\c S}erb{\u a}nu{\c t}{\u a}
    and Grigore Ro{\c s}u},
  title = {{jPredictor}: a predictive runtime analysis tool for {Java}},
  booktitle = {International Conference on Software Engineering (ICSE'08)},
  year = {2008},
  isbn = {978-1-60558-079-1},
  pages = {221-230},
  location = {Leipzig, Germany},
  doi = {http://doi.acm.org/10.1145/1368088.1368119},
  publisher = {ACM},
  address = {New York, NY, USA},
}

@inproceedings{meredith-jin-chen-rosu-2008-ase,
  title = {Efficient Monitoring of Parametric Context-Free Patterns},
  author = {Patrick Meredith and Dongyun Jin and Feng Chen and Grigore Ro\c{s}u},
  booktitle = {Automated Software Engineering (ASE '08)},
  year = {2008},
  publisher = {IEEE},
  pages = {148-157}
}

@inproceedings{chen-meredith-jin-rosu-2009-ase,
author = {F. Chen and P. Meredith and D. Jin and G. Ro\c{s}u},
title = {Efficient Formalism-Independent Monitoring of Parametric Properties},
booktitle = {Automated Software Engineering (ASE '09)},
Year       = {2009},
publisher = {IEEE},
note = {to appear}
}

@inproceedings{chen-rosu-2005-tacas,
author={Feng Chen and Grigore Ro\c{s}u},
title={{Java}-{MOP}: A Monitoring Oriented Programming Environment for {Java}},
booktitle={Tools and Algorithms for the Construction and Analysis of Systems (TACAS'05)},
series={LNCS},
volume={3440},
pages= {546-550},
year={2005}
}

@article{ruler,
	author = {Barringer, Howard   and Rydeheard, David   and Havelund, Klaus },
	journal = {J. Logic Computation},
	month = {November},
	pages = {exn076+},
	title = {Rule Systems for Run-time Monitoring: from EAGLE to RULER},
	year = {2008}
}

@article{Kozen,
title = "Results on the propositional [mu]-calculus",
journal = "J. Theoretical Computer Science",
volume = "27",
number = "3",
pages = "333 - 354",
year = "1983",
note = "",
issn = "0304-3975",
doi = "DOI: 10.1016/0304-3975(82)90125-6",
url = "http://www.sciencedirect.com/science/article/B6V1G-45TK9RG-T/2/91fe9ef25c099454365566642b762af4",
author = "Dexter Kozen"
}

@inproceedings{chen-rosu-2009-tacas,
  title={Parametric Trace Slicing and Monitoring},
  author={Feng Chen and Grigore Ro\c{s}u},
  booktitle={Tools and Algorithms for the Construction and Analysis of Systems (TACAS'09)},
  year={2009},
  series = {LNCS},
  volume = {5505},
  pages={246-261}
}

@misc{cfg-web,
	author = {P. Meredith and D. Jin and F. Chen and G. Ro\c{s}u},
	title = {{CFG Plugin} Website},
    note = {\url{http://fsl.cs.uiuc.edu/CFGPlugin}},
	 year = {2008}
}

@misc{tm-bench-march-2008,
  author = {E. Bodden and Patrick Lam and Laurie Hendren},
  title = {{Tracematches Benchmarks}},
  note = { {\url{http://abc.comlab.ox.ac.uk/tmahead}}},
  year = {2008}
}

@TechReport{CFG-tr,
author = {P. Meredith and D. Jin and F. Chen and G. Ro\c{s}u},
title = {Efficient Monitoring of Parametric Context-Free Patterns},
institution = {Department of Computer Science, University of Illinois at Urbana-Champaign},
Number     = {UIUCDCS-R-2008-2954},
Year       = {2008},
month      = {April}
}

@misc{javamop-online,
	author = {F. Chen and P. Meredith and D. Jin and G. Ro\c{s}u},
	title = {JavaMOP Online Trial Website},
    note = {\url{http://fsl.cs.uiuc.edu/index.php/Special:JavaMOPOnline}},
    year = 2007
}

@inproceedings{moore2000,
   author = {Robert C. Moore},
   title = {Removing left recursion from context-free grammars},
   booktitle = {The First Conference on North American Chapter of the Association for Computational Linguistics},
   year = {2000}
}

@inproceedings{aspectj-2001,
	title={An Overview of {AspectJ}},
	author = {Kiczales, Gregor   and Hilsdale, Erik   and Hugunin, Jim   and Kersten, Mik   and Palm, Jeffrey   and Griswold, William  G. },
	booktitle = {ECOOP'01},
	pages={327-353},
   series={LNCS},
	volume={2072},
	year = {2001}
}
			

@inproceedings{kiczales97aspectoriented,
    author = "Gregor Kiczales and John Lamping and Anurag Menhdhekar and Chris Maeda and Cristina Lopes and Jean-Marc Loingtier and John Irwin",
    title = "Aspect-Oriented Programming",
    booktitle = {ECOOP},
  series = "{LNCS}",
  volume = {1241},
  pages     = {220-242},
    year = "1997"
}

@inproceedings{Pal,
  title = "Instumenting {C} Programs with Nested Word Monitors",
  author = "Swarat Chaudhuri and Rajeev Alur",
  booktitle = "Model Checking Software(SPIN'07)",
  series = "{LNCS}",
  volume = "4595",
  pages = {279-283},
  year = "2007"
}

@inproceedings{slam01,
    author = "Thomas Ball and Sriram K. Rajamani",
    title = "Automatically Validating Temporal Safety Properties of Interfaces",
    booktitle = "Workshop on Model Checking of Software, SPIN 2001",
    year = "2001"
}

@book{acl2,
author = "Matt Kaufmann and Panagiotis Manolios and J Strother Moore",
title = "Computer-Aided Reasoning: ACL2 Case Studies",
publisher = "Kluwer Academic Publishers",
year = 2000
}

@inproceedings{chen-damorim-rosu-2005-rv,
title={Checking and Correcting Behaviors of {Java} Programs at Runtime with {JavaMOP}},
author="Feng Chen and Marcelo D'Amorim and Grigore Ro\c{s}u",
booktitle={Runtime Verification(RV'06)},
series={ENTCS},
volume = {144},
pages={3-20},
year={2006}
}

@inproceedings{chen-damorim-rosu-2004-icfem,
author={Feng Chen and Marcelo D'Amorim and Grigore Ro\c{s}u},
title={A Formal Monitoring-based Framework for Software Development and Analysis},
booktitle={Formal Engineering Methods (ICFEM'04)},
year={2004},
pages = {357-372},
series = {LNCS},
volume = {3308},
}

@misc{aspectj,
  key = "aspectj",
  title = {Aspect{J}},
  note = "http://eclipse.org/aspectj/"
}

@misc{eclipse,
  key = "eclipse",
  title = {Eclipse},
  note = "http://eclipse.org"
}

@misc{jhotdraw,
  key = "jhotdraw",
  title = {j{H}otdraw},
  note = "http://www.jhotdraw.org"
}

@misc{xalan,
  key = "xalan",
  title = {Xalan},
  note = "http://xml.apache.org/xalan-j/"
}

@UNPUBLISHED{maude2-manual,
    AUTHOR = {Manuel Clavel and Francisco Duran and Steven Eker and Patrick Lincoln and Narciso Mart-Oliet and Jose Meseguer and Carolyn Talcott},
    TITLE = {{Maude 2.0} {Manual}},
    NOTE = {http://maude.cs.uiuc.edu},
    url = {http://maude.cs.uiuc.edu}
}

@inproceedings{leavens00jml,
author = "Gary T. Leavens and K. Rustan M. Leino and Erik Poll and Clyde Ruby and Bart Jacobs",
title = {{JML}: notations and tools supporting detailed design in {Java}},
booktitle = {OOPSLA'00},
publisher = {ACM},
year = 2000,
pages = {105-106}
}

@inproceedings{cheon02runtime,
author = "Yoonsik Cheon and Gary T. Leavens",
title = {A {R}untime {A}ssertion {C}hecker for {JML}},
booktitle = "Software Engineering Research and Practice (SERP'02)",
year = "2002"
}

@inproceedings{rosu-viswanathan03,
author = "Grigore Ro\c{s}u and Mahesh Viswanathan",
title = "Testing {E}xtended {R}egular {L}anguage {M}embership {I}ncrementally by {R}ewriting",
booktitle = "Rewriting Techniques and Applications (RTA'03)",
year = "2003"
}

@inproceedings{sen-rosu03,
title = "Generating {O}ptimal {M}onitors for {E}xtended {R}egular {E}xpressions",
author = "K. Sen and G. Ro\c{s}u",
booktitle = "Runtime Verification(RV'03)",
year = 2003}

@inproceedings{pnueli77,
author = "Amir Pnueli",
title = {The Temporal Logic of Programs},
booktitle = "IEEE Symposium on Foundations of
  Computer Science",
year = 1977}

@inproceedings{havelund-rosu02,
title = "Synthesizing Monitors for Safety Properties",
author = "Klaus Havelund and Grigore Ro{\c s}u",
booktitle={Tools and Algorithms for the Construction and Analysis of Systems (TACAS'02)},
pages={342-356},
year = 2002}

@article{rosu-havelund-2005-jase,
  author    = {Grigore Ro\c{s}u and Klaus Havelund},
  title     = {Rewriting-Based Techniques for Runtime Verification.},
  journal   = {J. Automated Software Engineering},
  volume    = {12},
  number    = {2},
  year      = {2005},
  pages     = {151-197},
}

@book{havelund-rosuWSPS,
title = "Runtime Verification (RV'01, RV'02, RV'04)",
author = "Klaus Havelund and Grigore Ro\c{s}u",
year = "2001, 2002, 2004",
note = "ENTCS 55, 70, 113",
publisher = "Elsevier"
}

@book{sokolsky-viswanathan03,
title = "Runtime Verification (RV'03)",
author = "O. Sokolsky and M. Viswanathan",
note = "ENTCS 89",
year = 2003,
publisher = "Elsevier"
}

@book{rv05,
title = "Runtime Verification (RV'05)",
author = "Howard Barringer and Bernd Finkbeiner and Yuri Gurevich and Henny Sipma",
note = "ENTCS 144",
year = 2005,
publisher = "Elsevier"
}

@book{rv06,
title = "Formal Approaches to Testing and Runtime Verification (FATES/RV'06)",
author = "Klaus Havelund and Manuel Nunez and Grigore Rosu and Burkhart Wolff",
note = "LNCS 4262",
year = 2006
}

@book{oosc,
author = "B. Meyer",
title = {Object-Oriented Software Construction, {$2^{nd}$} edition},
publisher = "Prentice Hall",
address = "New Jersey",
year = "2000"}

@misc{eiffelsite,
key = "eiffel",
title = "Eiffel {L}anguage",
note = "http://www.eiffel.com/"}

@inproceedings{bartetzko01assertions,
    author = {Detlef Bartetzko and Clemens Fischer and Michael Moller and Heike Wehrheim},
    title = {Jass-{J}ava with {A}ssertions},
    booktitle = {Runtime Verification},
    series = {ENTCS},
volume    = {55.2},
    year = {2001}
}

@inproceedings{abercrombie02jcontractor,
author = {P. Abercrombie and M. Karaorman},
title = {j{C}ontractor: Bytecode Instrumentation Techniques for Implementing {DBC} in {J}ava},
booktitle = {Runtime Verification},
series = {ENTCS},
volume    = {70.4},
year = {2002}
}

@misc{timerover,
  author = "D. Drusinsky",
  title = "Temporal {R}over",
  note = {{\url{http://www.time-rover.com}}},
  year = {1997-2009}
}

@book{hoare,
author = "C.A.R. Hoare",
title = "Communicating Sequential Processes",
publisher = "Prentice-Hall Intl.",
address = "New York",
year = "1985"}

@article{java-mac04,
  author    = {MoonZoo Kim and
               Mahesh Viswanathan and
               Sampath Kannan and
               Insup Lee and
               Oleg Sokolsky},
  title     = {{Java-MaC}: A Run-Time Assurance Approach for {J}ava Programs},
  journal   = {Formal Methods in System Design},
  volume    = {24},
  number    = {2},
  pages     = {129-155},
  year      = {2004},
  ee        = {http://dx.doi.org/10.1023/B:FORM.0000017719.43755.7c},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@inproceedings{java-mac01,
title = {{Java-MaC}: a Runtime Assurance Tool for {Java}},
author = "M. Kim and S. Kannan and I. Lee and O. Sokolsky",
booktitle = {Runtime Verification},
year = 2001}

@book{monte-carlo,
author = "G.S. Fishman",
title = "Monte Carlo: Concepts, Algorithms, and Applicatioins",
publisher = "Springer Verlag",
year = 1995
}

@inproceedings{sha-simplex-94,
author = "L. Sha and R. Rajkumar and M. Gagliardi",
title = {The {SIMPLEX} architecture: An approach to build evolving industrial computing systems},
booktitle = "ISSAT Conference on Reliability",
year = 1994}

@misc{jboss,
  key = "jboss",
  title = {J{B}oss},
  note = "http://www.jboss.org"
}

@misc{aspectcc,
  key = "ApectC",
  title = {Aspect{C}++},
  note = "http://www.aspectc.org/",
}

@mastersthesis{j-lo,
author = "Eric Bodden",
title = "{J-LO}, a tool for runtime-checking temporal assertions",
year = 2005,
school = "RWTH Aachen University"
}

@article{asepct-intro,
 author = {Tzilla Elrad and Robert E. Filman and Atef Bader},
 title = {Aspect-oriented programming: Introduction},
 journal = {CACM},
 volume = {44},
 number = {10},
 year = {2001},
 pages = {29-32},
}

@article{speculative-exec,
 author = {Jean-Fran\&\#231;ois Collard},
 title = {Automatic parallelization of while-loops using speculative execution},
 journal = {Int. J. Parallel Program.},
 volume = {23},
 number = {2},
 year = {1995},
 pages = {191-219},
 publisher = {Kluwer Academic Publishers},
 }

@article{das-06,
 author = {Manuvir Das},
 title = {Unleashing the Power of Static Analysis},
 booktitle = {Static Analysis Symposium(SAS'06)},
 journal = {LNCS},
 volume = {4134},
 year = {2006},
 pages = {1-2},
 Note = "http://ropas.snu.ac.kr/sas06/program/sas06-das.ppt"
 }

@misc{javamop-web,
  key = "javamop",
  title = {{J}ava{MOP}},
  author = {Feng Chen and Grigore Ro\c{s}u},
  note = "http://fsl.cs.uiuc.edu/javamop"
}

@misc{lucene,
  key = "lucene",
  title = {Lucene},
  note = "http://lucene.apache.org"
}

@inproceedings{abc-05,
 author = {Pavel Avgustinov and Aske Simon Christensen and Laurie Hendren and Sascha Kuzins and Jennifer Lhotak and Ondrej Lhotak and Oege de Moor and Damien Sereni and Ganesh Sittampalam and Julian Tibble},
 title = {{A}{B}{C}: an extensible {A}spect{J} compiler},
 booktitle = {AOSD'05},
 publisher={ACM},
 year = {2005},
 pages = {87-98}
 }

@article{eagle-woda-05,
	 author = {Marcelo d'Amorim and Klaus Havelund},
	  title = {Event-based runtime verification of {J}ava programs},
	   journal = {ACM SIGSOFT Software Engineering Notes},
	    volume = {30},
		 number = {4},
		  year = {2005},
		   issn = {0163-5948},
		    pages = {1-7},
			    }

@inproceedings{marcelo-rosu-2005-cav,
 author = {Marcelo d'Amorim and Grigore Ro\c{s}u},
 title = {Efficient Monitoring of Omega-Languages},
 booktitle = {CAV'05},
 year = {2005},
 }

@misc{jtrek,
author = "S. Cohen",
title = "j{T}rek",
note = "Developed by Compaq"
}

@inproceedings{hackett-das-wang-yang-06,
 author = {Brian Hackett and Manuvir Das and Daniel Wang and Zhe Yang},
 title = {Modular checking for buffer overflows in the large},
 booktitle = {International Conference on Software engineering (ICSE'06)},
 year = {2006},
 }

@inproceedings{chen-rosu-2003-rv,
author={Feng Chen and Grigore Ro\c{s}u},
title={Towards Monitoring-Oriented Programming: A Paradigm Combining Specification and Implementation},
booktitle={Runtime Verification(RV'03)},
series = {ENTCS},
volume = {89},
year={2003}
}

@inproceedings{rosu-2003-asm,
author={C. Artho and D. Drusinsky and A. Goldberg and K. Havelund and M. Lowry and C. Pasareanu and G. Rosu and W. Visser},
title={Experiments with Test Case Generation and Runtime Analysis},
booktitle={ASM'03},
series = {LNCS},
volume = {2589},
pages = {87-107},
year={2003}
}

@inproceedings{rinard04enhancing,
  author = "M. Rinard and C. Cadar and D. Dumitran and D. Roy and T. Leu and J. Beebee",
  title = "Enhancing server availability and security through failure-oblivious computing",
  booktitle = "Symposium on Operating Systems Design and Implementation (OSDI'04)",
  year = "2004",
}

@inproceedings{rinard03acceptabilityoriented,
  author = "M. Rinard",
  title = "Acceptability-oriented computing",
  booktitle = "Onward! Track, OOPSLA'03",
  year = "2003",
}

@inproceedings{pql-oopsla,
  title = "Finding Application Errors and Security Flaws Using {PQL}: a Program Query Language",
  author = "Michael Martin and V. Benjamin Livshits and Monica S. Lam",
  booktitle = "OOPSLA'07",
  pages = {365-383},
  publisher={ACM},
  year = 2005
}

@inproceedings{barringer-eagle-04,
author = "H. Barringer and A. Goldberg and K. Havelund and K. Sen",
title = {Rule-{B}ased {R}untime {V}erification},
booktitle = "VMCAI'04",
series = {LNCS},
volume = {2937},
pages = {44-57},
year = 2004}

@inproceedings{specsharp-overview,
author = "Mike Barnett and K. Rustan M. Leino and Wolfram Schulte",
title = {The {S}pec\# programming system: An overview},
booktitle = {CASSIS'04},
series = {LNCS},
volume = {3362},
pages = {49-69},
year = 2004
}



@inproceedings{rosu-2007-fossacs,
author={Grigore Ro\c{s}u},
title={An Effective Algorithm for The Membership Problem for Extended Regular Expressions},
booktitle={Proceedings of the Tenth International Conference on Foundations Of Software Science and Computation Structures (FOSSACS'07)},
year={2007}
}

@inproceedings{havelund-rosu01c,
title = "Monitoring {J}ava Programs with {J}ava {P}ath{E}xplorer",
author = "Klaus Havelund and Grigore Ro\c{s}u",
series = {ENTCS},
volume = {55},
number = {2},
booktitle = {Runtime Verification(RV'01)},
year = {2001}
}

@inproceedings{tracematches-oopsla,
  author    = {Chris Allan and
               Pavel Avgustinov and
               Aske Simon Christensen and
               Laurie J. Hendren and
               Sascha Kuzins and
               Ondrej Lhot{\'a}k and
               Oege de Moor and
               Damien Sereni and
               Ganesh Sittampalam and
               Julian Tibble},
  title     = {Adding trace matching with free variables to {A}spect{J}},
  booktitle = {OOPSLA'05},
  publisher    = {ACM},
  year      = {2005},
  pages     = {345-364},
}

@inproceedings{ptql-oopsla,
 author = {Simon Goldsmith and Robert O'Callahan and Alex Aiken},
 title = {Relational queries over program traces},
 booktitle = {OOPSLA'05},
 publisher={ACM},
 pages = {385-402},
 year = {2005},
}

@InProceedings{DaCapo:paper,
  title={The {DaCapo} Benchmarks: {J}ava Benchmarking Development and Analysis},
  author={Blackburn, S. M. and Garner, R. and Hoffman, C. and Khan, A. M.
      and McKinley, K. S. and Bentzur, R. and Diwan, A. and Feinberg, D.
      and Frampton, D. and Guyer, S. Z. and Hirzel, M. and Hosking, A.
      and Jump, M. and Lee, H. and Moss, J. E. B. and Phansalkar, A.
      and Stefanovi\'{c}, D. and {VanDrunen}, T. and von~Dincklage, D.
      and Wiedermann, B.},
  booktitle = {OOPSLA'06},
  year = {2006},
  pages = {169-190},
  publisher={ACM}
}

@TechReport{tm-benchmark-tr,
author = {Pavel Avgustinov and Julian Tibble and Eric Bodden and Ondrej Lhotak and Laurie Hendren and Oege de Moor and Neil Ongkingco and Ganesh Sittampalam},
title = {Efficient Trace Monitoring},
institution = {Oxford University},
Number = {abc-2006-1},
Year       = {2006}
}

@book{metaobject,
author = "Gregor Kiczales and Jim Des Rivieres and Daniel G. Bobrow",
title = "The Art of the Metaobject Protocol",
publisher = "MIT Press",
year = 1991,
}

@article{schneider00,
  author    = {Fred B. Schneider},
  title     = {Enforceable security policies.},
  journal   = {ACM Transactions on Information System Security},
  volume    = {3},
  number    = {1},
  year      = {2000},
  pages     = {30-50},
}

@article{sql-injection,
author = {Chris Anley},
title = {Advanced {S}{Q}{L} Injection in {S}{Q}{L} Server Applications},
journal = {NGSSoftware},
year = {2002}
}

@InProceedings{tm-rv,
author = {Pavel Avgustinov and Eric Bodden and Elnar Hajiyev and Laurie Hendren and Ondrej Lhotak and Oege de Moor and Neil Ongkingco and Damien Sereni and Ganesh Sittampalam and Julian Tibble and Mathieu Verbaere},
title = {Aspects for Trace Monitoring},
booktitle = {FATES/RV'06},
volume = 4262,
pages = {20-39},
series = {LNCS},
year = 2006
}

@InProceedings{tm-static-ecoop,
  author = 	 {Eric Bodden and Laurie Hendren and Ond\v{r}ej Lhot{\'{a}}k},
  title = 	 {A Staged Static Program Analysis to Improve the Performance of Runtime Monitoring},
  booktitle = {ECOOP'07},
  year = {2007},
  series = {LNCS},
  volume = {4609},
  pages = {525-549}
}

@inproceedings{tm-oopsla-07,
author = {Pavel Avgustinov and Julian Tibble and Oege de Moor},
title = {Making Trace Monitors Feasible},
booktitle = {OOPSLA'07},
publisher={ACM},
pages = {589-608},
Year = {2007}
}

@TechReport{tm-static-tr2,
author = {Eric Bodden and Patrick Lam and Laurie Hendren},
title = {Flow-sensitive static optimizations for runtime monitors},
institution = {Oxford University},
Number = {abc-2007-3},
Year       = {2007}
}
@TechReport{rosu-2007-tr,
author = {Grigore Ro\c{s}u},
title = {On Safety Properties and Their Monitoring},
institution = {Dept. of Comp. Sci., Univ. of Illinois at Urbana-Champaign},
Number     = {UIUCDCS-R-2007-2850},
Year       = {2007}
}
@inproceedings{chen-rosu-2007-oopsla,
author = {Feng Chen and Grigore Ro\c{s}u},
title = {{MOP}: An Efficient and Generic Runtime Verification Framework},
booktitle = {OOPSLA'07},
year      = {2007},
publisher = {ACM},
pages = {569-588}
}

@Article{knuth65,
  author =       "Donald E. Knuth",
  title =        "On the translation of languages from left to right",
  journal =      "Information and Control",
  volume =       "8",
  number =       "6",
  pages =        "607-639",
  year =         "1965",
}

@book{aho-sethi-ullman-86,
 author = {Alfred V. Aho and Ravi Sethi and Jeffrey D. Ullman},
 title = {Compilers, principles, techniques, and tools},
 publisher = {Addison-Wesley},
 note = {pages 215-246},
 year = "1986"
}

@inproceedings{DBLP:conf/spin/ChaudhuriA07,
  author    = {Swarat Chaudhuri and
               Rajeev Alur},
  title     = {Instrumenting C Programs with Nested Word Monitors},
  booktitle = {SPIN'07},
  series    = {LNCS},
  volume    = {4595},
  pages     = {279-283},
  year      = {2007},
}

@TechReport{ptcaret-tr,
author = {anonymous authors},
title = {Synthesizing Monitors for Safety Properties \\-This Time With Calls and Returns-},
institution = {Dept. of Comp. Sci., University XYZ},
year = {2007},
note = {submitted for publication, available on request}
}

@article{pager-77,
  author    = {David Pager},
  title     = {A Practical General Method for Constructing {LR(k)} Parsers},
  journal   = {Acta Informatica},
  volume    = {7},
  year      = {1977},
  pages     = {249-268},
}

@manual{menhir,
	author={F. Pottier and Y. R\'{e}gis-Gianas},
	title = {Menhir Reference Manual},
	organization = {Institut National de Recherche en Informatique et en Automatique},
	year = {2007},
	URL = {\url{http://cristal.inria.fr/~fpottier/menhir/}}
}

@misc{bison,
    author = {A. Demaille and J. Denny and P. Eggert},
	 title =	{Bison},
	note = {{\url{http://www.gnu.org/software/bison}}},
	year = {2008}
}

@manual{ocamlex,
	author = {X. Leroy  with D. Doligez and J. Garrigue and D. R\'{e}my and J. Vouillon},
	title = {The Objective Caml system release 3.10},
	organization = {Institut National de Recherche en Informatique et en Automatique},
	year = {2006},
	URL = {\url{http://caml.inria.fr/pub/docs/manual-ocaml/index.html}}
}

@misc{javacc,
   key = "javacc",
   title = {{JavaCC} Documentation Index},
   year = {2007},
   URL = {\url{https://javacc.dev.java.net/doc/docindex.html}}
}
@book{hopcroft-motwani-ullman-01,
 author = {John E. Hopcroft and Rajeev Motwani and Jeffrey D. Ullman},
 title = {Introduction to automata theory, languages, and computation, $2^{nd}$ edition},
 year = {2001},
 publisher = {Addison-Wesley},
 }

@online{DNSSurvey,
   author = "The Measurement Factory",
   title = {{DNS} Survey: October 2010},
   year = 2010,
   url = {http://dns.measurement-factory.com/surveys/201010/},
   urldate = {2015-02-12}
}

@online{GooglePublicDNS,
   author = "Google Official Blog",
   title = {Google Public {DNS}: 70 billion requests a day and counting},
   year = 2012,
   url = {http://googleblog.blogspot.com/2012/02/google-public-dns-70-billion-requests.html},
   urldate = {2015-02-12}
}

@inproceedings {BIND-attack,
author = {Roee Hay and Jonathan Kalechstein and Gabi Nakibly},
title = {Subverting BIND{\textquoteright}s SRTT Algorithm Derandomizing NS Selection},
booktitle = {Presented as part of the 7th USENIX Workshop on Offensive Technologies},
year = {2013},
location = {Washington, D.C.},
url = {https://www.usenix.org/conference/woot13/workshop-program/presentation/Hay},
publisher = {USENIX},
}

@online{nginx,
  author = {Igor Sysoev},
  title = {nginx},
  url = {http://nginx.org/en/},
  urldate = {2015-02-24},
}
@online{CVE-2015-0057,
  author = "enSilo",
  title = {CVE-2015-0057: The 1-Bit that will Bring Windows Down},
  year = 2015,
  url = {https://www.ensilo.com/one-bit-rule-compromising-windows-single-bit/},
  urldate = {2015-02-24},
}

@online{Heartbleed-statistics,
   author = "Netcraft",
   title = {Half a million widely trusted websites vulnerable to Heartbleed bug},
   year = 2014,
   url = {http://news.netcraft.com/archives/2014/04/08/half-a-million-widely-trusted-websites-vulnerable-to-heartbleed-bug.html},
   urldate = {2015-02-12}
}

@inproceedings{hathhorn-ellison-rosu-2015-pldi,
   author = "Hathhorn, Chris and Ellison, Chucky and Ro\c{s}u, Grigore",
   publisher = "ACM",
   booktitle = "PLDI'15",
   pages = {336-345},
   year = "2015",
   title = "Defining the Undefinedness of {C}"
}

@inproceedings{klein2009sel4,
  title={seL4: Formal verification of an OS kernel},
  author={Klein, Gerwin and Elphinstone, Kevin and Heiser, Gernot and Andronick, June and Cock, David and Derrin, Philip and Elkaduwe, Dhammika and Engelhardt, Kai and Kolanski, Rafal and Norrish, Michael and others},
  booktitle={Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles},
  pages={207-220},
  year={2009},
  organization={ACM}
}

@online{lwip,
   author="Adam Dunkels",
   title = {lwIP-A Lightweight TCP/IP stack},
   year = "2012",
   url = {http://savannah.nongnu.org/projects/lwip/},
   urldate = {2015-02-23},
}

@online{musl,
   author={musl libc project},
   title = {musl libc},
   year = "2015",
   url = {http://www.musl-libc.org/},
   urldate = {2015-02-23},
}

@online{mbed-tls,
   author={ARM mbed},
   title = {SSL Library mbed TLS / PolarSSL},
   year = "2015",
   url = {https://tls.mbed.org/},
   urldate = {2015-02-23},
}

@phdthesis{black1998axiomatic,
  title={Axiomatic Semantics Veri2cation of a Secure Web Server},
  author={Black, Paul E},
  year={1998},
  school={Brigham Young University}
}

@online{cohen1996thttpd,
  title={Why is thttpd Secure?},
  author={Cohen, Frederick B},
  year={1996},
  url = {http://all.net/journal/white/walkthrough.html},
  urldate = {2015-02-23},
}

@online{acmethttpd,
  title = {thttpd-tiny/turbo/throttling HTTP server},
  author={ACME Labs},
  year = {2014},
  url= {http://acme.com/software/thttpd/},
  urldate = {2015-02-23},
}

@inproceedings{Affeldt:2002:FVM:1765533.1765553,
 author = {Affeldt, Reynald and Kobayashi, Naoki},
 title = {Formalization and Verification of a Mail Server in Coq},
 booktitle = {Proceedings of the 2002 Mext-NSF-JSPS International Conference on Software Security: Theories and Systems},
 series = {ISSS'02},
 year = {2003},
 isbn = {3-540-00708-3},
 location = {Tokyo, Japan},
 pages = {217-233},
 numpages = {17},
 url = {http://dl.acm.org/citation.cfm?id=1765533.1765553},
 acmid = {1765553},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
}

@inproceedings{chlipala-2015-popl,
  author = "Chlipala, Adam",
  publisher="ACM",
  booktitle = "Proceedings of the 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'15)",
  year = "2015",
  title = "From Network Interface to Multithreaded Web Applications: A Case Study in Modular Program Verification"
}

@online{netcraft-survey,
  title = "April 2014 Web Server Survey",
  author = "Netcraft",
  year = "2014",
  url = {http://news.netcraft.com/archives/2014/04/02/april-2014-web-server-survey.html},
  urldate={2015-02-23},
}

@techreport{c-standard,
  author={ISO/IEC},
  title = "Programming languages--{C}",
  type = "{ISO}",
  number="9899:2011",
  pages = {1-701},
  year = {2011},
  month = {December},
  publisher = "{ISO/IEC}",
  institution = {ISO/IEC WG14},
  url={http://www.open-std.org/JTC1/SC22/WG14/www/standards},
}

@inproceedings{DBLP:conf/tphol/CohenDHLMSST09,
  author    = {Ernie Cohen and
               Markus Dahlweid and
               Mark A. Hillebrand and
               Dirk Leinenbach and
               Michal Moskal and
               Thomas Santen and
               Wolfram Schulte and
               Stephan Tobies},
  title     = {{VCC:} {A} Practical System for Verifying Concurrent {C}},
  booktitle = {TPHOLs'09},
  year      = {2009},
  pages     = {23-42},
  series    = {LNCS},
  volume    = {5674},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/tphol/CohenDHLMSST09},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}


@inproceedings{DBLP:conf/esop/FilliatreP13,
  author    = {Jean{-}Christophe Filli{\^{a}}tre and
               Andrei Paskevich},
  title     = {Why3 - Where Programs Meet Provers},
  booktitle = {ESOP'13},
  year      = {2013},
  pages     = {125-128},
  series    = {LNCS},
  volume    = {7792},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/esop/FilliatreP13},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{stefanescu-ciobaca-mereuta-moore-serbanuta-rosu-2014-rta,
    author = "\c{S}tef\u{a}nescu, Andrei and Ciob\^{a}c\u{a}, \c{S}tefan and Mereu\c{t}\u{a}, Radu and Moore, Brandon M. and \c{S}erb\u{a}nu\c{t}\u{a}, Traian Florin and Ro\c{s}u, Grigore",
    publisher = "Springer",
    doi = "http://dx.doi.org/10.1007/978-3-319-08918-8_29",
    title = "All-Path Reachability Logic",
    series = "LNCS",
    booktitle = "RTA-TLCA'14",
    volume = "8560",
    year = "2014",
    pages = "425-440"
}

@inproceedings{bogdanas-rosu-2015-popl,
    author = "Bogd\u{a}na\c{s}, Denis and Ro\c{s}u, Grigore",
    publisher = "ACM",
    doi = "http://dx.doi.org/10.1145/2676726.2676982",
    title = "{K-Java: A Complete Semantics of Java}",
    booktitle = "POPL'15",
    month = "January",
    year = "2015",
    pages = "445-456"
}

@inproceedings{park-stefanescu-rosu-2015-pldi,
    author = "Park, Daejun and \c{S}tef\u{a}nescu, Andrei and Ro\c{s}u, Grigore",
    publisher = "ACM",
    booktitle = "PLDI'15",
    pages = "346-356",
    year = "2015",
    title = "{KJS}: A Complete Formal Semantics of {JavaScript}"
}
